OAI/Algebra/FormalGroup/Honda/Logarithm.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.HeightThree.LogarithmicConstruction.StrictLog line 14
  2. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.hasSubst line 23
  3. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.linear_unit line 26
  4. def OAI.HeightThree.LogarithmicConstruction.StrictLog.inv line 28
  5. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.inv_constant line 30
  6. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.inv_hasSubst line 33
  7. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.subst_inv line 36
  8. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.inv_subst line 39
  9. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.inv_linear line 42
  10. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.log_exp line 50
  11. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.exp_log line 55
  12. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.subst_injective line 60
  13. def OAI.HeightThree.LogarithmicConstruction.StrictLog.sumSeries line 66
  14. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.sumSeries_constant line 69
  15. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.sumSeries_hasSubst line 74
  16. def OAI.HeightThree.LogarithmicConstruction.StrictLog.law line 77
  17. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.law_constant line 79
  18. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.log_law line 82
  19. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.coeff_subst_linear line 85
  20. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.sumSeries_linear line 102
  21. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.law_linear line 109
  22. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.subst_after_mv line 114
  23. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.law_pair line 120
  24. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.law_pair_constant line 133
  25. lemma OAI.HeightThree.LogarithmicConstruction.StrictLog.log_law_pair line 140
  26. def OAI.HeightThree.LogarithmicConstruction.StrictLog.formalGroup line 148
  27. instance OAI.HeightThree.LogarithmicConstruction.StrictLog.formalGroup_isComm line 164