OAI/NumberTheory/PiExponent/Approximation/ClosedRestrictionTensor.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponent.ClosedRestrictionTensor.tensor_map_pure_val line 13
2. lemma OAI.PiExponent.ClosedRestrictionTensor.tensor_comm_pure_val line 20
3. lemma OAI.PiExponent.ClosedRestrictionTensor.projection_hom_pure_val line 25
4. lemma OAI.PiExponent.ClosedRestrictionTensor.pushforward_hom_pure_val line 34
5. def OAI.PiExponent.ClosedRestrictionTensor.powerProjectionIso line 44
6. def OAI.PiExponent.ClosedRestrictionTensor.powerUnit line 50
7. lemma OAI.PiExponent.ClosedRestrictionTensor.powerProjectionIso_succ_pure line 55
8. lemma OAI.PiExponent.ClosedRestrictionTensor.powerUnit_succ_pure line 82
9. theorem OAI.PiExponent.ClosedRestrictionTensor.twist_structureMap_power line 117
10. theorem OAI.PiExponent.ClosedRestrictionTensor.power_restriction_eq line 152
11. theorem OAI.PiExponent.ClosedRestrictionTensor.push_pullbackSection line 164
12. theorem OAI.PiExponent.ClosedRestrictionTensor.section_restriction_eq line 186