OAI/RingTheory/Multiplicity/ScalarExtensionDepth.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.extendScalars_range_le line 14
2. lemma OAI.Lech.frobenius_minimal_depth line 41
3. lemma OAI.Lech.acyclic_of_unit_nullhomotopy line 54
4. lemma OAI.Lech.baseChange_map_smul line 60
5. def OAI.Lech.baseChange_nullhomotopy line 73
6. lemma OAI.Lech.short_extension_acyclicAway line 87