IdealQuotient

Statistics

Metric	Count
Definitions `quotientEquivDirectSum`, `quotientEquivPiSpan`, `quotientEquivPiZMod`	3
Theorems `finiteQuotientOfFreeOfNeBot`, `finrank_quotient_eq_sum`	2
Total	5

Name	Kind	Assumes	Proves	Validates	Depends On
`finiteQuotientOfFreeOfNeBot` 📖	mathematical	—	`Finite` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1`	—	`Submodule.finiteQuotientOfFreeOfRankEq` `IsScalarTower.right` `finrank_eq_finrank` `Int.instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `Finite.of_fintype`
`finrank_quotient_eq_sum` 📖	mathematical	`Module.Free` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1` `span` `Set` `Set.instSingletonSet` `smithCoeffs` `Finite.of_fintype` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Quotient.commRing` `Submodule.Quotient.module'` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `Algebra.toSMul` `Algebra.toModule` `IsScalarTower.right` `Module.Finite`	`Module.finrank` `Finset.sum` `Nat.instAddCommMonoid` `Finset.univ`	—	`Finite.of_fintype` `IsScalarTower.right` `LinearEquiv.finrank_eq` `Module.finrank_directSum` `commRing_strongRankCondition`

---