OAI/NumberTheory/PiExponent/Jets/NormalFrameBasis.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.NormalBasisRigidity.frameEquiv line 12
2. def OAI.PiExponent.NormalBasisRigidity.frameBasis line 39
3. lemma OAI.PiExponent.NormalBasisRigidity.frameBasis_repr_zero line 42
4. lemma OAI.PiExponent.NormalBasisRigidity.frameBasis_repr_succ line 48
5. lemma OAI.PiExponent.NormalBasisRigidity.frameBasis_succ line 54
6. lemma OAI.PiExponent.NormalBasisRigidity.frameBasis_zero_zero line 61
7. lemma OAI.PiExponent.NormalBasisRigidity.frameBasis_zero_succ line 64
8. lemma OAI.PiExponent.NormalBasisRigidity.mandatory_logarithmic_differential line 69
9. lemma OAI.PiExponent.NormalBasisRigidity.span_mapped_basis_eq_top line 78
10. theorem OAI.PiExponent.NormalBasisRigidity.normal_basis_differential_dichotomy line 91