Documentation Verification Report

Lattice

📁 Source: Mathlib/Algebra/Module/Lattice.lean

Statistics

Metric	Count
Definitions `extendOfIsLattice`, `IsLattice`	2
Theorems `extendOfIsLattice_apply`, `fg`, `finite`, `finrank_of_pi`, `free`, `inf`, `of_le_of_isLattice_of_fg`, `of_rank_le`, `rank'`, `rank_of_pi`, `smul`, `span_eq_top`, `sup`, `span_range_eq_top_of_injective_of_rank_le`	14
Total	16

Module.Basis

Definitions

Name	Category	Theorems
`extendOfIsLattice` 📖	CompOp	1 math math: `extendOfIsLattice_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extendOfIsLattice_apply` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `instFunLike` `extendOfIsLattice` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	—

Submodule

Definitions

Name	Category	Theorems
`IsLattice` 📖	CompData	5 math math: `IsLattice.of_le_of_isLattice_of_fg`, `IsLattice.smul`, `IsLattice.inf`, `IsLattice.sup`, `IsLattice.of_rank_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`span_range_eq_top_of_injective_of_rank_le` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `Cardinal` `Cardinal.instLE` `Module.rank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`span` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `SetLike.coe` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `setLike` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Top.top` `instTop`	—	`RingHomSurjective.ids` `exists_set_linearIndependent` `IsDomain.hasRankNullity` `LinearIndependent.map'` `LinearMap.ker_eq_bot` `le_antisymm` `LinearIndependent.cardinal_le_rank` `EuclideanDomain.toNontrivial` `LinearIndependent.iff_fractionRing` `Cardinal.mk_eq_nat_iff_fintype` `Module.finrank_eq_rank` `IsNoetherianRing.strongRankCondition` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `eq_top_iff` `LinearIndependent.span_eq_top_of_card_eq_finrank'` `span_mono`

Submodule.IsLattice

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg` 📖	mathematical	—	`Submodule.FG` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	—
`finite` 📖	mathematical	—	`Module.Finite` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	`Module.Finite.iff_fg` `fg`
`finrank_of_pi` 📖	mathematical	—	`Module.finrank` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Pi.Function.module` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `Fintype.card`	—	`Pi.isScalarTower` `IsScalarTower.right` `Module.finrank_eq_of_rank_eq` `rank_of_pi`
`free` 📖	mathematical	—	`Module.Free` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	`Module.IsTorsionFree.trans_faithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `EuclideanDomain.toNontrivial` `IsDomain.toNontrivial` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Module.free_of_finite_type_torsion_free'` `finite` `Ideal.instIsTorsionFreeSubtypeMemSubmodule`
`inf` 📖	mathematical	—	`Submodule.IsLattice` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AddCommGroup.toAddCommMonoid` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instMin`	—	`isNoetherian_of_le` `isNoetherian_of_isNoetherianRing_of_finite` `PrincipalIdealRing.isNoetherianRing` `finite` `inf_le_left` `Module.Finite.iff_fg` `Module.IsNoetherian.finite` `RingHomSurjective.ids` `Submodule.range_subtype` `Submodule.span_range_eq_top_of_injective_of_rank_le` `Submodule.injective_subtype` `Submodule.rank_sup_add_rank_inf_eq` `IsDomain.hasRankNullity` `Cardinal.eq_of_add_eq_add_left` `rank'` `sup` `Module.rank_lt_aleph0` `IsNoetherianRing.strongRankCondition` `EuclideanDomain.toNontrivial` `EuclideanDomain.to_principal_ideal_domain` `le_refl`
`of_le_of_isLattice_of_fg` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.FG`	`Submodule.IsLattice` `AddCommGroup.toAddCommMonoid`	—	`eq_top_iff` `le_trans` `span_eq_top` `le_refl` `Submodule.span_mono`
`of_rank_le` 📖	mathematical	`Submodule.FG` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Cardinal` `Cardinal.instLE` `Module.rank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	`Submodule.IsLattice` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AddCommGroup.toAddCommMonoid`	—	`RingHomSurjective.ids` `Submodule.range_subtype` `Submodule.span_range_eq_top_of_injective_of_rank_le` `Submodule.injective_subtype`
`rank'` 📖	mathematical	—	`Module.rank` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`free` `FaithfulSMul.to_isTorsionFree` `IsFractionRing.instFaithfulSMul` `IsDomain.toNontrivial` `IsDomain.toIsCancelMulZero` `instIsDomain` `finite` `rank_eq_card_basis` `IsNoetherianRing.strongRankCondition` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.toNontrivial` `EuclideanDomain.to_principal_ideal_domain`
`rank_of_pi` 📖	mathematical	—	`Module.rank` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Pi.Function.module` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `Cardinal` `Cardinal.instNatCast` `Fintype.card`	—	`Pi.isScalarTower` `IsScalarTower.right` `rank'` `rank_pi` `IsNoetherianRing.strongRankCondition` `EuclideanDomain.toNontrivial` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `Module.free_of_finite_type_torsion_free'` `instIsDomain` `FiniteDimensional.finiteDimensional_self` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Finite.of_fintype` `Module.rank_self` `Cardinal.sum_const` `Cardinal.mk_fintype` `Cardinal.lift_natCast` `Cardinal.lift_one` `mul_one`
`smul` 📖	mathematical	—	`Submodule.IsLattice` `AddCommGroup.toAddCommMonoid` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule` `Units.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Submodule.pointwiseAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Submodule.pointwiseDistribMulAction` `Module.toDistribMulAction` `IsScalarTower.to_smulCommClass'`	—	`IsScalarTower.to_smulCommClass'` `fg` `Units.smulCommClass_left` `Submodule.smul_span` `Finite.Set.finite_image` `Finite.of_fintype` `Submodule.fg_span` `Set.toFinite` `Submodule.coe_pointwise_smul` `smulCommClass_self` `span_eq_top` `Submodule.ext` `smul_inv_smul` `Submodule.smul_mem_pointwise_smul`
`span_eq_top` 📖	mathematical	—	`Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.coe` `Submodule` `Submodule.setLike` `Top.top` `Submodule.instTop`	—	—
`sup` 📖	mathematical	—	`Submodule.IsLattice` `AddCommGroup.toAddCommMonoid` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	—	`of_le_of_isLattice_of_fg` `le_sup_left` `Submodule.FG.sup` `fg`

---

← Back to Index