OAI/NumberTheory/PiExponent/Jets/NormalBasisRigidity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.NormalBasisRigidity.IsNormalBasis line 13
2. lemma OAI.PiExponent.NormalBasisRigidity.exists_normalBasis_subset line 16
3. lemma OAI.PiExponent.NormalBasisRigidity.exists_normalBasis_containing line 28
4. lemma OAI.PiExponent.NormalBasisRigidity.IsNormalBasis.ne_zero line 41
5. lemma OAI.PiExponent.NormalBasisRigidity.exists_normalBasis_omitting line 45
6. lemma OAI.PiExponent.NormalBasisRigidity.mandatory_not_mem_span line 51
7. lemma OAI.PiExponent.NormalBasisRigidity.IsNormalBasis.card_eq line 68
8. lemma OAI.PiExponent.NormalBasisRigidity.mandatory_coordinate_eq_zero line 81
9. lemma OAI.PiExponent.NormalBasisRigidity.largest_nontangent_mandatory line 105
10. lemma OAI.PiExponent.NormalBasisRigidity.weighted_normalBasis_exclusion line 128
11. lemma OAI.PiExponent.NormalBasisRigidity.normalBasis_unique_of_discrepancy_excluded line 143