Documentation Verification Report

Quotient

📁 Source: Mathlib/LinearAlgebra/FreeModule/Finite/Quotient.lean

Statistics

Metric	Count
Definitions `quotientEquivDirectSum`, `quotientEquivPiSpan`, `quotientEquivPiZMod`	3
Theorems `finiteQuotientOfFreeOfRankEq`, `finiteQuotient_iff`, `finrank_quotient_eq_sum`	3
Total	6

Submodule

Definitions

Name	Category	Theorems
`quotientEquivDirectSum` 📖	CompOp	—
`quotientEquivPiSpan` 📖	CompOp	—
`quotientEquivPiZMod` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finiteQuotientOfFreeOfRankEq` 📖	mathematical	`Module.finrank` `Submodule` `Int.instSemiring` `AddCommGroup.toAddCommMonoid` `AddCommGroup.toIntModule` `SetLike.instMembership` `setLike` `addCommMonoid` `addCommGroup` `Int.instRing`	`Finite` `HasQuotient.Quotient` `Submodule` `Int.instSemiring` `AddCommGroup.toAddCommMonoid` `AddCommGroup.toIntModule` `hasQuotient` `Int.instRing`	—	`Int.instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `Finite.of_fintype` `smithNormalFormCoeffs_ne_zero` `Finite.of_equiv` `Pi.finite`
`finiteQuotient_iff` 📖	mathematical	—	`Finite` `HasQuotient.Quotient` `Submodule` `Int.instSemiring` `AddCommGroup.toAddCommMonoid` `AddCommGroup.toIntModule` `hasQuotient` `Int.instRing` `Module.finrank` `SetLike.instMembership` `setLike` `addCommMonoid` `addCommGroup`	—	`le_antisymm` `finrank_le` `commRing_strongRankCondition` `Int.instNontrivial` `LinearMap.finrank_le_finrank_of_injective` `Module.IsNoetherian.finite` `isNoetherian_submodule'` `isNoetherian_of_isNoetherianRing_of_finite` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `smulCommClass_self` `natCast_zsmul` `neg_mem` `AddSubgroup.nsmul_index_mem` `AddSubgroup.normal_of_comm` `Function.Injective.codRestrict` `LinearMap.lsmul_injective` `Int.instIsDomain` `Module.Free.instIsTorsionFree` `Nat.card_ne_zero` `Set.nonempty_iff_univ_nonempty` `Set.univ_nonempty` `finiteQuotientOfFreeOfRankEq`
`finrank_quotient_eq_sum` 📖	mathematical	`Module.finrank` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `Module.Free` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient_1` `Ideal.span` `Set` `Set.instSingletonSet` `smithNormalFormCoeffs` `Finite.of_fintype` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Quotient.module'` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `Algebra.toSMul` `Algebra.toModule` `IsScalarTower.right` `Module.Finite`	`Module.finrank` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `hasQuotient` `CommRing.toRing` `Quotient.addCommGroup` `Quotient.module'` `Algebra.toSMul` `Finset.sum` `Nat.instAddCommMonoid` `Finset.univ` `Ideal` `Ideal.instHasQuotient_1` `Ideal.span` `Set` `Set.instSingletonSet` `smithNormalFormCoeffs` `Finite.of_fintype` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Ring.toAddCommGroup` `Semiring.toModule` `Algebra.toModule` `IsScalarTower.right`	—	`Finite.of_fintype` `IsScalarTower.right` `LinearEquiv.finrank_eq` `Module.finrank_directSum` `commRing_strongRankCondition`

---

← Back to Index