OAI/Algebra/FormalGroup/Honda/Jets.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HeightThree.HondaJets.EqJet line 12
  2. lemma OAI.HeightThree.HondaJets.eqJet_iff_order line 15
  3. lemma OAI.HeightThree.HondaJets.eqJet_iff_trunc line 23
  4. lemma OAI.HeightThree.HondaJets.EqJet.refl line 33
  5. lemma OAI.HeightThree.HondaJets.EqJet.symm line 34
  6. lemma OAI.HeightThree.HondaJets.EqJet.trans line 36
  7. lemma OAI.HeightThree.HondaJets.EqJet.mono line 38
  8. lemma OAI.HeightThree.HondaJets.EqJet.add line 40
  9. lemma OAI.HeightThree.HondaJets.EqJet.sub line 43
  10. lemma OAI.HeightThree.HondaJets.EqJet.neg line 46
  11. lemma OAI.HeightThree.HondaJets.EqJet.mul_left line 48
  12. lemma OAI.HeightThree.HondaJets.EqJet.mul_right line 53
  13. lemma OAI.HeightThree.HondaJets.EqJet.mul line 55
  14. lemma OAI.HeightThree.HondaJets.EqJet.sum line 58
  15. lemma OAI.HeightThree.HondaJets.EqJet.subst_left line 62
  16. lemma OAI.HeightThree.HondaJets.EqJet.subst_right line 72
  17. lemma OAI.HeightThree.HondaJets.eqJet_zero_mul line 82
  18. lemma OAI.HeightThree.HondaJets.eqJet_one_zero line 87
  19. lemma OAI.HeightThree.HondaJets.eqJet_sub_zero line 91
  20. lemma OAI.HeightThree.HondaJets.eqJet_subst_constant line 96
  21. lemma OAI.HeightThree.HondaJets.coeff_linear_mul line 104
  22. lemma OAI.HeightThree.HondaJets.subst_first_order_polynomial line 112
  23. lemma OAI.HeightThree.HondaJets.subst_first_order line 152
  24. lemma OAI.HeightThree.HondaJets.law_first_order line 178
  25. lemma OAI.HeightThree.HondaJets.EqJet.mul_leading line 186
  26. lemma OAI.HeightThree.HondaJets.eqJet_pow_zero line 198
  27. lemma OAI.HeightThree.HondaJets.EqJet.pow_leading line 203
  28. lemma OAI.HeightThree.HondaJets.leading_part line 212
  29. lemma OAI.HeightThree.HondaJets.homogeneous_eq_of_jet line 221
  30. lemma OAI.HeightThree.HondaJets.subst_homogeneous_leading line 232
  31. lemma OAI.HeightThree.HondaJets.homogeneous_subst_linear line 253