OAI/RingTheory/Multiplicity/FiniteModuleTensor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.length_scalar_cokernel_pi_module line 12
2. lemma OAI.Lech.length_module_isogeny line 32
3. lemma OAI.Lech.length_le_quotient_generators line 81
4. lemma OAI.Lech.length_scalar_cokernel_le_generators line 107
5. lemma OAI.Lech.tensor_length_isogeny line 134
6. theorem OAI.Lech.finite_module_tensor_compare line 169
7. theorem OAI.Lech.finite_module_tensor_asymptoticENN line 208