OAI/Algebra/FormalGroup/Honda/SmallExtension.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.HeightThree.SmallExtension.IsSmall line 12
  2. lemma OAI.HeightThree.SmallExtension.IsSmall.squareZero line 16
  3. lemma OAI.HeightThree.SmallExtension.subst_eq_of_annihilate line 19
  4. lemma OAI.HeightThree.SmallExtension.unisubst_eq_of_annihilate line 38
  5. lemma OAI.HeightThree.SmallExtension.series_mul_zero line 45
  6. lemma OAI.HeightThree.SmallExtension.highPower_eq line 57
  7. lemma OAI.HeightThree.SmallExtension.subst_expand_inner line 68
  8. lemma OAI.HeightThree.SmallExtension.law_perturbation line 76
  9. lemma OAI.HeightThree.SmallExtension.series_perturbation line 103
  10. def OAI.HeightThree.SmallExtension.point line 122
  11. lemma OAI.HeightThree.SmallExtension.multiplication_at_point line 124
  12. lemma OAI.HeightThree.SmallExtension.multiplication_preserves_addition line 144
  13. lemma OAI.HeightThree.SmallExtension.multiplication_reduction line 164
  14. theorem OAI.HeightThree.SmallExtension.linearized_p_hom line 173
  15. lemma OAI.HeightThree.SmallExtension.series_map_zero_of_ker_le line 248
  16. lemma OAI.HeightThree.SmallExtension.coordinate_of_coboundary line 256
  17. lemma OAI.HeightThree.SmallExtension.multiplication_linear line 312
  18. lemma OAI.HeightThree.SmallExtension.power_expand_iterate line 321
  19. theorem OAI.HeightThree.SmallExtension.small_equivalence_of_matching_parameters line 334
  20. lemma OAI.HeightThree.SmallExtension.small_isomorphism_pseries line 385
  21. lemma OAI.HeightThree.SmallExtension.small_isomorphism_lowcoeff line 416
  22. lemma OAI.HeightThree.SmallExtension.small_automorphism_rigid line 427