OAI/Algebra/AffineCancellation/QuotientDerivation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ComplexCancellation.QuotientDerivation.linear line 12
  2. lemma OAI.ComplexCancellation.QuotientDerivation.linear_mk line 16
  3. def OAI.ComplexCancellation.QuotientDerivation.derivation line 19
  4. lemma OAI.ComplexCancellation.QuotientDerivation.derivation_mk line 27
  5. lemma OAI.ComplexCancellation.QuotientDerivation.iterate_mk line 30
  6. lemma OAI.ComplexCancellation.QuotientDerivation.locallyNilpotent line 38
  7. lemma OAI.ComplexCancellation.QuotientDerivation.span_singleton_stable line 45