OAI/RingTheory/Multiplicity/DuttaBaseChange.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.frobeniusBaseChangeIso line 14
2. lemma OAI.Lech.flat_homology_length line 32
3. lemma OAI.Lech.dimension_eq_of_map_maximalIdeal line 55
4. lemma OAI.Lech.duttaSequence_baseChange line 60
5. lemma OAI.Lech.shortComplex_baseChange line 73