Basic

Statistics

Metric	Count
Definitions	0
Theorems `rank_quotient_eq_of_le_torsion`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`rank_quotient_eq_of_le_torsion` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.torsion`	`Module.rank` `HasQuotient.Quotient` `Submodule.hasQuotient` `CommRing.toRing` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	—	`LE.le.antisymm` `rank_quotient_le` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `rank_subsingleton` `Module.rank_def` `ciSup_le` `nonempty_linearIndependent_set` `LinearIndependent.cardinal_le_rank` `Finset.sum_congr` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `Subtype.prop` `linearIndependent_iff'` `LinearIndepOn.eq_1` `smul_smul` `Finset.smul_sum` `mul_comm`

---