Documentation Verification Report

PrimaryComponent

📁 Source: Mathlib/Algebra/Module/Torsion/PrimaryComponent.lean

Statistics

Metric	Count
Definitions `primaryComponent`, `map`	2
Theorems `map_ker_eq`, `primaryComponent_map_mem`, `primaryComponent_mem`, `primaryComponent_sup`, `primaryComponent_torsionBySet_eq_inf`, `primaryComponent_torsionBySet_of_isCoprime`	6
Total	8

Ideal

Definitions

Name	Category	Theorems
`primaryComponent` 📖	CompOp	6 math math: `primaryComponent_sup`, `primaryComponent_map_mem`, `primaryComponent_mem`, `primaryComponent.map_ker_eq`, `primaryComponent_torsionBySet_of_isCoprime`, `primaryComponent_torsionBySet_eq_inf`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`primaryComponent_map_mem` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `primaryComponent` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	`SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`primaryComponent_mem` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `primaryComponent` `Submodule.torsionBySet` `SetLike.coe` `Ideal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id`	—	`Submodule.mem_iSup_of_directed` `Submodule.mem_iSup_of_mem`
`primaryComponent_sup` 📖	mathematical	`Disjoint` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `Submodule.instOrderBot`	`Submodule.map` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.subtype` `primaryComponent`	—	`Submodule.ext` `RingHomSurjective.ids` `SMulMemClass.smul_mem` `Submodule.smulMemClass` `Submodule.disjoint_iff_add_eq_zero` `Submodule.smul_mem` `smul_add` `pow_le_pow_right` `add_zero`
`primaryComponent_torsionBySet_eq_inf` 📖	mathematical	—	`Submodule.map` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.torsionBySet` `SetLike.coe` `Ideal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `RingHomSurjective.ids` `Submodule.subtype` `primaryComponent` `Submodule.instMin`	—	`Submodule.ext` `RingHomSurjective.ids` `SMulMemClass.smul_mem` `Submodule.smulMemClass`
`primaryComponent_torsionBySet_of_isCoprime` 📖	mathematical	`IsCoprime` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring`	`primaryComponent` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.torsionBySet` `SetLike.coe` `Ideal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.addCommMonoid` `Submodule.module` `Bot.bot` `Submodule.instBot`	—	`IsScalarTower.right` `Submodule.disjoint_torsionBySet_ideal` `pow_sup_eq_top` `instIsTwoSided_1` `IsCoprime.sup_eq` `Submodule.map_injective_of_injective` `RingHomSurjective.ids` `Submodule.subtype_injective` `Submodule.ext` `SMulMemClass.smul_mem` `Submodule.smulMemClass` `Submodule.map_bot` `smul_zero`

Ideal.primaryComponent

Definitions

Name	Category	Theorems
`map` 📖	CompOp	1 math math: `map_ker_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_ker_eq` 📖	mathematical	—	`Submodule.map` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `Ideal.primaryComponent` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.subtype` `LinearMap.ker` `map`	—	`RingHomSurjective.ids` `Submodule.ext`

---

← Back to Index