OAI/NumberTheory/PiExponent/Approximation/TensorSectionOpen.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponentSeshadri.Geometry.tensorFrame line 16
2. def OAI.PiExponentSeshadri.TensorPure.tensorSection line 31
3. lemma OAI.PiExponentSeshadri.TensorPure.section_apply line 35
4. lemma OAI.PiExponentSeshadri.TensorPure.framed_pure line 52
5. lemma OAI.PiExponentSeshadri.TensorPure.local_framed_pure line 61
6. lemma OAI.PiExponentSeshadri.TensorPure.local_section_coefficient line 73
7. lemma OAI.PiExponentSeshadri.TensorPure.section_open line 88