OAI/Algebra/AffineCancellation/Extraction.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ComplexCancellation.AffineModification.coefficient_injective line 12
  2. lemma OAI.ComplexCancellation.AffineModification.τ_nonzero line 18
  3. lemma OAI.ComplexCancellation.AffineModification.V_nonzero line 25
  4. def OAI.ComplexCancellation.AffineModification.coefficientHom line 31
  5. lemma OAI.ComplexCancellation.AffineModification.coefficientHom_injective line 33
  6. def OAI.ComplexCancellation.AffineModification.eulerPoly line 36
  7. lemma OAI.ComplexCancellation.AffineModification.eulerPoly_relation line 39
  8. def OAI.ComplexCancellation.AffineModification.euler line 46
  9. lemma OAI.ComplexCancellation.AffineModification.euler_π line 52
  10. lemma OAI.ComplexCancellation.AffineModification.euler_coefficient line 55
  11. lemma OAI.ComplexCancellation.AffineModification.euler_τ line 61
  12. lemma OAI.ComplexCancellation.AffineModification.euler_V line 64
  13. lemma OAI.ComplexCancellation.AffineModification.euler_monomial line 67
  14. lemma OAI.ComplexCancellation.AffineModification.derivation_zero_of_generators line 79