OAI/RingTheory/Multiplicity/ScalarHomologyError.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.scalar_range_eq line 13
2. lemma OAI.Lech.scalar_comp_quotientπ line 20
3. def OAI.Lech.scalarQuotientShortComplex line 30
4. lemma OAI.Lech.scalarQuotientShortExact line 34
5. lemma OAI.Lech.scalarHomologyKer line 49
6. def OAI.Lech.scalarHomologyCokernelEmbedding line 68
7. lemma OAI.Lech.scalarHomologyCokernelEmbedding_injective line 77
8. lemma OAI.Lech.homology_kernel_killed_of_scalar_retract line 87
9. lemma OAI.Lech.homology_length_le_of_scalar_retract line 100
10. lemma OAI.Lech.normalized_homology_length_le_of_scalar_retract line 121