OAI/Algebra/AffineCancellation/ReesDerivation.lean
11 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ComplexCancellation.Rees.uniform_clearline 11 - lemma
OAI.ComplexCancellation.Rees.stable_of_generatorsline 18 - lemma
OAI.ComplexCancellation.Rees.clear_annihilateline 37 - lemma
OAI.ComplexCancellation.Rees.scaled_is_lnline 52 - lemma
OAI.ComplexCancellation.Rees.scaled_fixesline 56 - lemma
OAI.ComplexCancellation.Rees.restrict_stableline 67 - lemma
OAI.ComplexCancellation.Rees.scaled_restrictionline 75 - def
OAI.ComplexCancellation.Rees.upline 98 - lemma
OAI.ComplexCancellation.Rees.red_upline 99 - lemma
OAI.ComplexCancellation.Rees.red_surjectiveline 104 - lemma
OAI.ComplexCancellation.Rees.primitive_reductionline 108