OAI/RingTheory/Multiplicity/RootLineEuler.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.SplitPair.left line 12
  2. def OAI.Lech.SplitPair.right line 21
  3. lemma OAI.Lech.SplitPair.left_injective line 29
  4. lemma OAI.Lech.SplitPair.right_surjective line 38
  5. lemma OAI.Lech.SplitPair.exact line 46
  6. def OAI.Lech.RootInvariants.coordinateMul line 77
  7. lemma OAI.Lech.RootInvariants.coordinateMul_val line 84
  8. def OAI.Lech.RootInvariants.eulerLeft line 90
  9. def OAI.Lech.RootInvariants.eulerRight line 95
  10. def OAI.Lech.RootInvariants.eulerMiddleEquiv line 103
  11. lemma OAI.Lech.RootInvariants.tensorEquiv_coordinateMul line 108
  12. lemma OAI.Lech.RootInvariants.eulerLeft_base_compat line 124
  13. lemma OAI.Lech.RootInvariants.eulerRight_base_compat line 140
  14. lemma OAI.Lech.RootInvariants.eulerLeft_injective line 154
  15. lemma OAI.Lech.RootInvariants.eulerRight_surjective line 165
  16. lemma OAI.Lech.RootInvariants.euler_exact line 181