Basic

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

Statistics

Metric	Count
Definitions `torsionBy`, `zmodModule`, `torsionByStx`, `torsionByUnexpander`, `quotTorsionOfEquivSpanSingleton`, `torsionOf`, `IsTorsion`, `IsTorsion'`, `IsTorsionBy`, `hasSMul`, `IsTorsionBySet`, `hasSMul`, `semilinearMap`, `instQuotientIdealSpanSingletonSetSubmoduleHSMulTop`, `instQuotientIdealSpanSubmoduleHSMulSetTop`, `instQuotientIdealSubmoduleHSMulTop`, `quotientAnnihilator`, `instDistribMulActionSubtypeMemTorsion'`, `instModuleQuotientIdealSpanSingletonSetSubtypeMemTorsionBy`, `instModuleQuotientIdealSubtypeMemTorsionBySetCoe`, `instModuleQuotientTorsionBy`, `instSMulSubtypeMemTorsion'`, `pOrder`, `submodule_torsionBy_orderIso`, `torsion`, `torsion'`, `torsionBy`, `torsionBySet`	28
Theorems `isTorsion_iff_isTorsion_int`, `isTorsion_iff_isTorsion_nat`, `mod_self_nsmul`, `mod_self_nsmul'`, `neg`, `nsmul`, `nsmul_iff`, `torsionBy_eq_span_singleton`, `coe_torsionOf`, `linearIndependent'`, `mem_torsionOf_iff`, `quotTorsionOfEquivSpanSingleton_apply_mk`, `torsionOf_eq_bot_iff_of_noZeroSMulDivisors`, `torsionOf_eq_top_iff`, `torsionOf_zero`, `mk_smul`, `quotient`, `isScalarTower`, `isSemisimpleModule_iff`, `mk_smul`, `quotient`, `mk_smul_mk`, `isTorsionBySet_annihilator`, `isTorsionBySet_annihilator_top`, `isTorsionBySet_iff_is_torsion_by_span`, `isTorsionBySet_iff_subset_annihilator`, `isTorsionBySet_iff_subseteq_ker_lsmul`, `isTorsionBySet_iff_torsionBySet_eq_top`, `isTorsionBySet_of_subset`, `isTorsionBySet_quotient_ideal_smul`, `isTorsionBySet_quotient_iff`, `isTorsionBySet_quotient_set_smul`, `isTorsionBySet_singleton_iff`, `isTorsionBySet_span_singleton_iff`, `isTorsionBy_iff_mem_annihilator`, `isTorsionBy_iff_mem_ker_lsmul`, `isTorsionBy_iff_torsionBy_eq_top`, `isTorsionBy_quotient_element_smul`, `isTorsionBy_quotient_iff`, `instIsTorsionFree`, `torsion_eq_bot`, `annihilator_top_inter_nonZeroDivisors`, `coe_torsion'`, `coe_torsionBy`, `coe_torsionBySet`, `coe_torsion_eq_annihilator_ne_bot`, `exists_isTorsionBy`, `iSup_torsionBySet_ideal_eq_torsionBySet_iInf`, `iSup_torsionBy_eq_torsionBy_prod`, `instIsScalarTowerQuotientIdealSubtypeMemTorsionBySetCoe`, `instIsScalarTowerQuotientSpanSingletonSetSubtypeMemTorsionBy`, `instSMulCommClassSubtypeMemTorsion'`, `isTorsion'_iff_torsion'_eq_top`, `isTorsion'_powers_iff`, `isTorsionFree_iff_torsion_eq_bot`, `mem_torsion'_iff`, `mem_torsionBySet_iff`, `mem_torsionBy_iff`, `mem_torsion_iff`, `pow_pOrder_smul`, `smul_coe`, `smul_coe_torsionBy`, `smul_torsionBy`, `supIndep_torsionBy`, `supIndep_torsionBySet_ideal`, `torsion'_isTorsion'`, `torsion'_torsion'_eq_top`, `mk_ideal_smul`, `mk_smul`, `mk_smul`, `torsionBySet_eq_torsionBySet_span`, `torsionBySet_isInternal`, `torsionBySet_isTorsionBySet`, `torsionBySet_le_torsionBySet_of_subset`, `torsionBySet_singleton_eq`, `torsionBySet_span_singleton_eq`, `torsionBySet_torsionBySet_eq_top`, `torsionBySet_univ`, `torsionBy_isInternal`, `torsionBy_isTorsionBy`, `torsionBy_le_torsionBy_of_dvd`, `torsionBy_one`, `torsionBy_torsionBy_eq_top`, `torsion_gc`, `torsion_int`, `torsion_isTorsion`, `torsion_torsion_eq_top`, `infinite_range_add_nsmul_iff`, `infinite_range_add_smul_iff`, `isSMulRegular_iff_torsionBy_eq_bot`	90
Total	118

AddMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isTorsion_iff_isTorsion_int` 📖	mathematical	—	`IsTorsion` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.IsTorsion` `Int.instSemiring` `AddCommGroup.toAddCommMonoid` `AddCommGroup.toIntModule`	—	`IsOfFinAddOrder.exists_nsmul_eq_zero` `mem_nonZeroDivisors_of_ne_zero` `IsStrictOrderedRing.noZeroDivisors` `Int.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `ne_of_gt` `natCast_zsmul` `isOfFinAddOrder_iff_nsmul_eq_zero` `nonZeroDivisors.coe_ne_zero` `Int.instNontrivial` `natAbs_nsmul_eq_zero`
`isTorsion_iff_isTorsion_nat` 📖	mathematical	—	`IsTorsion` `AddCommMonoid.toAddMonoid` `Module.IsTorsion` `Nat.instSemiring` `AddCommMonoid.toNatModule`	—	`IsOfFinAddOrder.exists_nsmul_eq_zero` `mem_nonZeroDivisors_of_ne_zero` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `ne_of_gt` `isOfFinAddOrder_iff_nsmul_eq_zero` `nonZeroDivisors.coe_ne_zero` `Nat.instNontrivial`

AddSubgroup

Definitions

Name	Category	Theorems
`torsionBy` 📖	CompOp	4 math math: `torsionBy.mod_self_nsmul`, `torsionBy.nsmul_iff`, `torsionBy.neg`, `torsionBy.nsmul`
`torsionByStx` 📖	CompOp	—
`torsionByUnexpander` 📖	CompOp	—

AddSubgroup.torsionBy

Definitions

Name	Category	Theorems
`zmodModule` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mod_self_nsmul` 📖	mathematical	—	`AddSubgroup` `AddCommGroup.toAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.torsionBy` `AddSubgroup.nsmul`	—	`nsmul_eq_mod_nsmul` `nsmul`
`mod_self_nsmul'` 📖	mathematical	`AddSubgroup` `AddCommGroup.toAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.torsionBy`	`AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`nsmul_eq_mod_nsmul` `nsmul_iff`
`neg` 📖	mathematical	—	`AddSubgroup.torsionBy`	—	`AddSubgroup.ext` `neg_smul`
`nsmul` 📖	mathematical	—	`AddSubgroup` `AddCommGroup.toAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.torsionBy` `AddSubgroup.nsmul` `AddSubgroup.zero`	—	`Submodule.smul_torsionBy` `Nat.cast_smul_eq_nsmul`
`nsmul_iff` 📖	mathematical	—	`AddSubgroup` `AddCommGroup.toAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.torsionBy` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Submodule.mem_torsionBy_iff` `Nat.cast_smul_eq_nsmul`

Ideal

Definitions

Name	Category	Theorems
`quotTorsionOfEquivSpanSingleton` 📖	CompOp	1 math math: `quotTorsionOfEquivSpanSingleton_apply_mk`
`torsionOf` 📖	CompOp	7 math math: `torsionOf_eq_span_pow_pOrder`, `torsionOf_zero`, `torsionOf_eq_top_iff`, `mem_torsionOf_iff`, `coe_torsionOf`, `torsionOf_eq_bot_iff_of_noZeroSMulDivisors`, `quotTorsionOfEquivSpanSingleton_apply_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_torsionOf` 📖	mathematical	—	`SetLike.coe` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.setLike` `torsionOf` `Set.preimage` `DFunLike.coe` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `LinearMap.toSpanSingleton` `Set` `Set.instSingletonSet` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`mem_torsionOf_iff` 📖	mathematical	—	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `torsionOf` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—
`quotTorsionOfEquivSpanSingleton_apply_mk` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `HasQuotient.Quotient` `Ideal` `instHasQuotient` `torsionOf` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set` `Set.instSingletonSet` `Submodule.Quotient.addCommGroup` `Ring.toAddCommGroup` `Semiring.toModule` `Submodule.addCommMonoid` `Submodule.Quotient.module` `Submodule.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `quotTorsionOfEquivSpanSingleton` `Submodule.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Submodule.mem_span_singleton_self`	—	`RingHomInvPair.ids`
`torsionOf_eq_bot_iff_of_noZeroSMulDivisors` 📖	mathematical	—	`torsionOf` `Bot.bot` `Ideal` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`bot_ne_top` `instNontrivial` `IsDomain.toNontrivial` `torsionOf_zero` `Submodule.eq_bot_iff` `smul_eq_zero` `IsDomain.toIsCancelMulZero` `mem_torsionOf_iff`
`torsionOf_eq_top_iff` 📖	mathematical	—	`torsionOf` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`one_smul` `mem_torsionOf_iff` `Submodule.mem_top` `torsionOf_zero`
`torsionOf_zero` 📖	mathematical	—	`torsionOf` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`LinearMap.toSpanSingleton_zero` `LinearMap.ker_zero`

Ideal.Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`torsionBy_eq_span_singleton` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	`Submodule.torsionBy` `HasQuotient.Quotient` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `Ideal.instHasQuotient_1` `Submodule.span` `Set` `Set.instSingletonSet` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `commRing` `Submodule.Quotient.module` `CommRing.toRing` `Ring.toAddCommGroup` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `RingHom` `ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike`	—	`Submodule.ext` `Ideal.instIsTwoSided_1` `Submodule.mem_torsionBy_iff` `Submodule.mem_span_singleton` `mk_surjective` `Submodule.Quotient.mk_eq_zero` `Submodule.Quotient.mk_smul` `mul_comm` `mul_cancel_left_mem_nonZeroDivisors` `mul_assoc` `smul_eq_mul` `SMulCommClass.smul_comm` `Submodule.Quotient.smulCommClass` `Algebra.to_smulCommClass` `Ideal.mem_span_singleton_self` `smul_zero`

Ideal.iSupIndep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearIndependent'` 📖	mathematical	`iSupIndep` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.completeLattice` `Submodule.span` `Set` `Set.instSingletonSet` `Ideal.torsionOf` `Bot.bot` `Ideal` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`LinearIndependent`	—	`linearIndependent_iff_eq_zero_of_smul_mem_span` `iSupIndep_def` `iSup_subtype'` `Submodule.span_range_eq_iSup` `Submodule.mem_inf` `Submodule.mem_span_singleton` `Set.ext` `Submodule.mem_bot`

Module

Definitions

Name	Category	Theorems
`IsTorsion` 📖	MathDef	7 math math: `AEval.isTorsion_of_aeval_eq_zero`, `AEval.isTorsion_of_finiteDimensional`, `rank_eq_zero_iff_isTorsion`, `AddMonoid.isTorsion_iff_isTorsion_int`, `AddMonoid.isTorsion_iff_isTorsion_nat`, `Submodule.torsion_isTorsion`, `finrank_eq_zero_iff_isTorsion`
`IsTorsion'` 📖	MathDef	3 math math: `Submodule.isTorsion'_powers_iff`, `Submodule.isTorsion'_iff_torsion'_eq_top`, `Submodule.torsion'_isTorsion'`
`IsTorsionBy` 📖	MathDef	9 math math: `Submodule.exists_isTorsionBy`, `isTorsionBySet_span_singleton_iff`, `isTorsionBySet_singleton_iff`, `isTorsionBy_iff_mem_ker_lsmul`, `isTorsionBy_quotient_iff`, `Submodule.torsionBy_isTorsionBy`, `isTorsionBy_iff_mem_annihilator`, `isTorsionBy_iff_torsionBy_eq_top`, `isTorsionBy_quotient_element_smul`
`IsTorsionBySet` 📖	MathDef	13 math math: `isTorsionBySet_quotient_set_smul`, `isTorsionBySet_quotient_ideal_smul`, `isTorsionBySet_annihilator`, `Ideal.isTorsionBySet_cotangent`, `isTorsionBySet_iff_torsionBySet_eq_top`, `isTorsionBySet_span_singleton_iff`, `isTorsionBySet_singleton_iff`, `isTorsionBySet_iff_subseteq_ker_lsmul`, `isTorsionBySet_iff_is_torsion_by_span`, `isTorsionBySet_annihilator_top`, `isTorsionBySet_quotient_iff`, `isTorsionBySet_iff_subset_annihilator`, `Submodule.torsionBySet_isTorsionBySet`
`instQuotientIdealSpanSingletonSetSubmoduleHSMulTop` 📖	CompOp	2 math math: `RingTheory.Sequence.isWeaklyRegular_cons_iff'`, `RingTheory.Sequence.isRegular_cons_iff'`
`instQuotientIdealSpanSubmoduleHSMulSetTop` 📖	CompOp	—
`instQuotientIdealSubmoduleHSMulTop` 📖	CompOp	7 math math: `AdicCompletion.map_val_apply`, `AdicCompletion.val_smul_eq_evalₐ_smul`, `AdicCompletion.pi_apply_coe`, `Quotient.mk_smul_mk`, `AdicCompletion.transitionMap_comp_reduceModIdeal`, `RingTheory.Sequence.isWeaklyRegular_append_iff'`, `LinearMap.reduceModIdeal_apply`
`quotientAnnihilator` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isTorsionBySet_annihilator` 📖	mathematical	—	`IsTorsionBySet` `SetLike.coe` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `annihilator`	—	`mem_annihilator`
`isTorsionBySet_annihilator_top` 📖	mathematical	—	`IsTorsionBySet` `CommSemiring.toSemiring` `SetLike.coe` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.annihilator` `Top.top` `Submodule` `Submodule.instTop`	—	`Submodule.mem_annihilator` `Subtype.prop` `Submodule.mem_top`
`isTorsionBySet_iff_is_torsion_by_span` 📖	mathematical	—	`IsTorsionBySet` `SetLike.coe` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.span`	—	`Ideal.span_le`
`isTorsionBySet_iff_subset_annihilator` 📖	mathematical	—	`IsTorsionBySet` `Set` `Set.instHasSubset` `SetLike.coe` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `annihilator`	—	`SetCoe.forall`
`isTorsionBySet_iff_subseteq_ker_lsmul` 📖	mathematical	—	`IsTorsionBySet` `CommSemiring.toSemiring` `Set` `Set.instHasSubset` `SetLike.coe` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.setLike` `LinearMap.ker` `LinearMap` `RingHom.id` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `toDistribMulAction` `LinearMap.lsmul`	—	`smulCommClass_self` `LinearMap.mem_ker` `LinearMap.ext` `DFunLike.congr_fun`
`isTorsionBySet_iff_torsionBySet_eq_top` 📖	mathematical	—	`IsTorsionBySet` `CommSemiring.toSemiring` `Submodule.torsionBySet` `Top.top` `Submodule` `Submodule.instTop`	—	`eq_top_iff` `Submodule.mem_torsionBySet_iff`
`isTorsionBySet_of_subset` 📖	—	`Set` `Set.instHasSubset` `IsTorsionBySet`	—	—	—
`isTorsionBySet_quotient_ideal_smul` 📖	mathematical	—	`IsTorsionBySet` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Ideal` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `toDistribMulAction` `Top.top` `Submodule.instTop` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `SetLike.coe` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`IsScalarTower.left` `isTorsionBySet_quotient_iff` `Submodule.smul_mem_smul`
`isTorsionBySet_quotient_iff` 📖	mathematical	—	`IsTorsionBySet` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `SetLike.instMembership` `Submodule.setLike` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `toDistribMulAction`	—	`Function.Surjective.forall` `Submodule.mkQ_surjective` `Submodule.Quotient.mk_eq_zero`
`isTorsionBySet_quotient_set_smul` 📖	mathematical	—	`IsTorsionBySet` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Set` `Submodule.pointwiseSetSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `toDistribMulAction` `Top.top` `Submodule.instTop` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	—	`isTorsionBySet_quotient_iff` `Submodule.mem_set_smul_of_mem_mem` `Submodule.mem_top`
`isTorsionBySet_singleton_iff` 📖	mathematical	—	`IsTorsionBySet` `Set` `Set.instSingletonSet` `IsTorsionBy`	—	`Set.mem_singleton`
`isTorsionBySet_span_singleton_iff` 📖	mathematical	—	`IsTorsionBySet` `SetLike.coe` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.setLike` `Submodule.span` `Set` `Set.instSingletonSet` `IsTorsionBy`	—	`isTorsionBySet_iff_is_torsion_by_span` `isTorsionBySet_singleton_iff`
`isTorsionBy_iff_mem_annihilator` 📖	mathematical	—	`IsTorsionBy` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `annihilator`	—	`IsTorsionBy.eq_1` `mem_annihilator`
`isTorsionBy_iff_mem_ker_lsmul` 📖	mathematical	—	`IsTorsionBy` `CommSemiring.toSemiring` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.ker` `LinearMap` `RingHom.id` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `toDistribMulAction` `LinearMap.lsmul`	—	`smulCommClass_self` `LinearMap.ext_iff`
`isTorsionBy_iff_torsionBy_eq_top` 📖	mathematical	—	`IsTorsionBy` `CommSemiring.toSemiring` `Submodule.torsionBy` `Top.top` `Submodule` `Submodule.instTop`	—	`Submodule.torsionBySet_singleton_eq` `isTorsionBySet_singleton_iff` `isTorsionBySet_iff_torsionBySet_eq_top`
`isTorsionBy_quotient_element_smul` 📖	mathematical	—	`IsTorsionBy` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `CommRing.toRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Submodule.pointwiseAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Submodule.pointwiseDistribMulAction` `toDistribMulAction` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `Top.top` `Submodule.instTop` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	—	`smulCommClass_self` `isTorsionBy_quotient_iff` `Submodule.smul_mem_pointwise_smul`
`isTorsionBy_quotient_iff` 📖	mathematical	—	`IsTorsionBy` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `SetLike.instMembership` `Submodule.setLike` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `toDistribMulAction`	—	`Function.Surjective.forall` `Submodule.mkQ_surjective` `Submodule.Quotient.mk_eq_zero`

Module.IsTorsionBy

Definitions

Name	Category	Theorems
`hasSMul` 📖	CompOp	1 math math: `mk_smul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_smul` 📖	mathematical	`Module.IsTorsionBy` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	`HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `hasSMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `RingHom.instFunLike` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—
`quotient` 📖	mathematical	`Module.IsTorsionBy` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	`HasQuotient.Quotient` `Submodule` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	—	`Module.isTorsionBy_quotient_iff` `Submodule.zero_mem`

Module.IsTorsionBySet

Definitions

Name	Category	Theorems
`hasSMul` 📖	CompOp	1 math math: `mk_smul`
`semilinearMap` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isScalarTower` 📖	mathematical	`Module.IsTorsionBySet` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.coe` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`IsScalarTower` `HasQuotient.Quotient` `Ideal.instHasQuotient` `Submodule.Quotient.instSMul'` `Ring.toAddCommGroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ideal.Quotient.ring` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `module`	—	`Quotient.inductionOn'` `smul_assoc`
`isSemisimpleModule_iff` 📖	mathematical	`Module.IsTorsionBySet` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.coe` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`IsSemisimpleModule` `HasQuotient.Quotient` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `module`	—	`LinearMap.isSemisimpleModule_iff_of_bijective` `Ideal.Quotient.instRingHomSurjectiveQuotientMk` `Function.bijective_id`
`mk_smul` 📖	mathematical	`Module.IsTorsionBySet` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.coe` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`HasQuotient.Quotient` `Ideal.instHasQuotient` `hasSMul` `DFunLike.coe` `RingHom` `Ideal.Quotient.ring` `RingHom.instFunLike` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—
`quotient` 📖	mathematical	`Module.IsTorsionBySet` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	`HasQuotient.Quotient` `Submodule` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	—	`Module.isTorsionBySet_quotient_iff` `Submodule.zero_mem`

Module.Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_smul_mk` 📖	mathematical	—	`HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `Submodule` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Top.top` `Submodule.instTop` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Submodule.Quotient.addCommGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Ideal.Quotient.ring` `Module.instQuotientIdealSubmoduleHSMulTop` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`IsScalarTower.left`

Submodule

Definitions

Name	Category	Theorems
`instDistribMulActionSubtypeMemTorsion'` 📖	CompOp	1 math math: `torsion'_torsion'_eq_top`
`instModuleQuotientIdealSpanSingletonSetSubtypeMemTorsionBy` 📖	CompOp	1 math math: `torsionBy.mk_ideal_smul`
`instModuleQuotientIdealSubtypeMemTorsionBySetCoe` 📖	CompOp	2 math math: `instIsScalarTowerQuotientIdealSubtypeMemTorsionBySetCoe`, `torsionBySet.mk_smul`
`instModuleQuotientTorsionBy` 📖	CompOp	2 math math: `instIsScalarTowerQuotientSpanSingletonSetSubtypeMemTorsionBy`, `torsionBy.mk_smul`
`instSMulSubtypeMemTorsion'` 📖	CompOp	3 math math: `torsion'_isTorsion'`, `instSMulCommClassSubtypeMemTorsion'`, `smul_coe`
`pOrder` 📖	CompOp	3 math math: `pow_pOrder_smul`, `exists_isTorsionBy`, `Ideal.torsionOf_eq_span_pow_pOrder`
`submodule_torsionBy_orderIso` 📖	CompOp	—
`torsion` 📖	CompOp	12 math math: `mem_torsion_iff`, `torsion_int`, `torsion_torsion_eq_top`, `Module.Flat.torsion_eq_bot`, `Module.Flat.flat_iff_torsion_eq_bot_of_valuationRing_localization_isMaximal`, `Module.Flat.flat_iff_torsion_eq_bot_of_isBezout`, `QuotientTorsion.instIsTorsionFree`, `isTorsionFree_iff_torsion_eq_bot`, `coe_torsion_eq_annihilator_ne_bot`, `torsion_isTorsion`, `QuotientTorsion.torsion_eq_bot`, `IsDedekindDomain.flat_iff_torsion_eq_bot`
`torsion'` 📖	CompOp	7 math math: `coe_torsion'`, `isTorsion'_iff_torsion'_eq_top`, `torsion'_torsion'_eq_top`, `torsion'_isTorsion'`, `instSMulCommClassSubtypeMemTorsion'`, `mem_torsion'_iff`, `smul_coe`
`torsionBy` 📖	CompOp	22 math math: `isInternal_prime_power_torsion_of_pid`, `isSemisimple_torsionBy_of_irreducible`, `torsionBySet_singleton_eq`, `torsionBy_torsionBy_eq_top`, `smul_coe_torsionBy`, `isSMulRegular_iff_torsionBy_eq_bot`, `Ideal.Quotient.torsionBy_eq_span_singleton`, `instIsScalarTowerQuotientSpanSingletonSetSubtypeMemTorsionBy`, `exists_isInternal_prime_power_torsion_of_pid`, `torsionBy.mk_ideal_smul`, `coe_torsionBy`, `supIndep_torsionBy`, `torsionBySet_span_singleton_eq`, `iSup_torsionBy_eq_torsionBy_prod`, `torsionBy_one`, `mem_torsionBy_iff`, `smul_torsionBy`, `torsionBy_isTorsionBy`, `torsionBy_le_torsionBy_of_dvd`, `torsionBy_isInternal`, `Module.isTorsionBy_iff_torsionBy_eq_top`, `torsionBy.mk_smul`
`torsionBySet` 📖	CompOp	19 math math: `instIsScalarTowerQuotientIdealSubtypeMemTorsionBySetCoe`, `supIndep_torsionBySet_ideal`, `torsionBySet_singleton_eq`, `torsionBySet_le_torsionBySet_of_subset`, `isInternal_prime_power_torsion_of_is_torsion_by_ideal`, `mem_torsionBySet_iff`, `Module.isTorsionBySet_iff_torsionBySet_eq_top`, `torsionBySet_isInternal`, `coe_torsionBySet`, `torsionBySet_torsionBySet_eq_top`, `torsionBySet_span_singleton_eq`, `torsion_gc`, `exists_isInternal_prime_power_torsion`, `isInternal_prime_power_torsion`, `torsionBySet_univ`, `iSup_torsionBySet_ideal_eq_torsionBySet_iInf`, `torsionBySet_eq_torsionBySet_span`, `torsionBySet.mk_smul`, `torsionBySet_isTorsionBySet`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`annihilator_top_inter_nonZeroDivisors` 📖	mathematical	`Module.IsTorsion` `CommSemiring.toSemiring`	`Set.Nonempty` `Set` `Set.instInter` `SetLike.coe` `Ideal` `setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `annihilator` `Top.top` `Submodule` `instTop` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Submonoid.instSetLike` `nonZeroDivisors`	—	`Module.Finite.fg_top` `Submonoid.coe_finset_prod` `SetLike.mem_coe` `mem_annihilator_span` `Finset.prod_erase_mul` `Subtype.prop` `SemigroupAction.mul_smul` `Submonoid.smul_def` `smul_zero`
`coe_torsion'` 📖	mathematical	—	`SetLike.coe` `Submodule` `CommSemiring.toSemiring` `setLike` `torsion'` `setOf` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `CommMonoid.toMonoid`	—	—
`coe_torsionBy` 📖	mathematical	—	`SetLike.coe` `Submodule` `CommSemiring.toSemiring` `setLike` `torsionBy` `Set.preimage` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `DistribSMul.toLinearMap` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Set` `Set.instSingletonSet` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—
`coe_torsionBySet` 📖	mathematical	—	`SetLike.coe` `Submodule` `CommSemiring.toSemiring` `setLike` `torsionBySet` `Set.iInter` `Set` `Set.instMembership` `Set.preimage` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `DistribSMul.toLinearMap` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Set.instSingletonSet` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`Set.iInter_congr_Prop` `Set.iInter_exists` `Set.biInter_and'` `Set.iInter_iInter_eq_right`
`coe_torsion_eq_annihilator_ne_bot` 📖	mathematical	—	`SetLike.coe` `Submodule` `CommSemiring.toSemiring` `setLike` `torsion` `setOf` `Ideal` `annihilator` `span` `Set` `Set.instSingletonSet` `Bot.bot` `instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`Set.ext` `SMulCommClass.smul_comm` `smulCommClass_self` `Submonoid.smul_def` `smul_zero` `nonZeroDivisors.coe_ne_zero` `mem_nonZeroDivisors_of_ne_zero` `one_smul`
`exists_isTorsionBy` 📖	mathematical	`Module.IsTorsion'` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.powers` `Submonoid.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Module.toDistribMulAction` `span` `Set.range` `Top.top` `Submodule` `instTop`	`Module.IsTorsionBy` `Monoid.toNatPow` `pOrder`	—	`List.argmax_eq_none` `Module.isTorsionBy_iff_torsionBy_eq_top` `eq_top_iff` `span_le` `Set.range_subset_iff` `List.le_of_mem_argmax` `pow_add` `SemigroupAction.mul_smul` `pow_pOrder_smul` `smul_zero`
`iSup_torsionBySet_ideal_eq_torsionBySet_iInf` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Ideal` `CommSemiring.toSemiring` `SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `idemSemiring` `Algebra.id` `Top.top` `instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`iSup` `Submodule` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `Finset.instMembership` `torsionBySet` `setLike` `iInf` `instInfSet`	—	`Finset.eq_empty_or_nonempty` `iSup_congr_Prop` `iSup_neg` `iSup_bot` `iInf_congr_Prop` `iInf_neg` `iInf_top` `torsionBySet_univ` `le_antisymm` `iSup_le` `torsionBySet_le_torsionBySet_of_subset` `LE.le.trans` `iInf_le` `mem_iSup_finset_iff_exists_sum` `Ideal.eq_top_iff_one` `Ideal.iSup_iInf_eq_top_iff_pairwise` `mem_torsionBySet_iff` `smul_smul` `mem_iInf` `Ideal.mul_mem_right` `Ideal.instIsTwoSided` `coe_mem` `Ideal.mul_mem_left` `Finset.sum_smul` `one_smul`
`iSup_torsionBy_eq_torsionBy_prod` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.onFun` `IsCoprime`	`iSup` `Submodule` `CommSemiring.toSemiring` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `Finset.instMembership` `torsionBy` `Finset.prod` `CommSemiring.toCommMonoid`	—	`torsionBySet_span_singleton_eq` `Ideal.submodule_span_eq` `Ideal.finset_inf_span_singleton` `Finset.inf_eq_iInf` `iSup_torsionBySet_ideal_eq_torsionBySet_iInf` `Ideal.sup_eq_top_iff_isCoprime`
`instIsScalarTowerQuotientIdealSubtypeMemTorsionBySetCoe` 📖	mathematical	—	`IsScalarTower` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `torsionBySet` `SetLike.coe` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Quotient.instSMul'` `CommRing.toRing` `Ring.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ideal.Quotient.semiring` `Module.toDistribMulAction` `addCommMonoid` `instModuleQuotientIdealSubtypeMemTorsionBySetCoe` `smul`	—	`Module.IsTorsionBySet.isScalarTower` `Ideal.instIsTwoSided_1` `isScalarTower'` `IsScalarTower.left`
`instIsScalarTowerQuotientSpanSingletonSetSubtypeMemTorsionBy` 📖	mathematical	—	`IsScalarTower` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `Ideal.instHasQuotient_1` `span` `Set` `Set.instSingletonSet` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `torsionBy` `Quotient.instSMul'` `CommRing.toRing` `Ring.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ideal.Quotient.semiring` `Module.toDistribMulAction` `addCommMonoid` `instModuleQuotientTorsionBy` `smul`	—	`Module.IsTorsionBySet.isScalarTower` `Ideal.instIsTwoSided_1` `isScalarTower'` `IsScalarTower.left`
`instSMulCommClassSubtypeMemTorsion'` 📖	mathematical	—	`SMulCommClass` `Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `torsion'` `instSMulSubtypeMemTorsion'` `smul` `Algebra.toSMul` `Algebra.id` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.left` `DistribMulAction.toMulAction`	—	`IsScalarTower.left` `SMulCommClass.smul_comm`
`isTorsion'_iff_torsion'_eq_top` 📖	mathematical	—	`Module.IsTorsion'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `CommMonoid.toMonoid` `torsion'` `Top.top` `Submodule` `CommSemiring.toSemiring` `instTop`	—	`eq_top_iff` `mem_torsion'_iff`
`isTorsion'_powers_iff` 📖	mathematical	—	`Module.IsTorsion'` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.powers` `Submonoid.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Monoid.toNatPow`	—	—
`isTorsionFree_iff_torsion_eq_bot` 📖	mathematical	—	`Module.IsTorsionFree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `torsion` `Bot.bot` `Submodule` `instBot`	—	`IsDomain.to_noZeroDivisors` `IsDomain.toNontrivial` `Set.instReflSubset` `Set.instAntisymmSubset` `smul_zero`
`mem_torsion'_iff` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `torsion'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `CommMonoid.toMonoid`	—	—
`mem_torsionBySet_iff` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `torsionBySet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Set` `Set.instMembership`	—	`mem_sInf` `Set.mem_image_of_mem`
`mem_torsionBy_iff` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `torsionBy` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—
`mem_torsion_iff` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `torsion` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Submonoid.instSetLike` `nonZeroDivisors` `Submonoid.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Module.toDistribMulAction`	—	—
`pow_pOrder_smul` 📖	mathematical	`Module.IsTorsion'` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.powers` `Submonoid.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	`Monoid.toNatPow` `pOrder`	—	`Nat.find_spec` `isTorsion'_powers_iff`
`smul_coe` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `torsion'` `instSMulSubtypeMemTorsion'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `CommMonoid.toMonoid`	—	—
`smul_coe_torsionBy` 📖	mathematical	—	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `Submodule` `SetLike.instMembership` `setLike` `torsionBy`	—	`Subtype.prop`
`smul_torsionBy` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `torsionBy` `smul` `Algebra.toSMul` `Algebra.id` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.left` `DistribMulAction.toMulAction` `zero`	—	`IsScalarTower.left` `Subtype.prop`
`supIndep_torsionBy` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.onFun` `IsCoprime`	`Finset.SupIndep` `Submodule` `CommSemiring.toSemiring` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `instOrderBot` `torsionBy`	—	`torsionBySet_span_singleton_eq` `supIndep_torsionBySet_ideal` `Ideal.sup_eq_top_iff_isCoprime`
`supIndep_torsionBySet_ideal` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Ideal` `CommSemiring.toSemiring` `SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `idemSemiring` `Algebra.id` `Top.top` `instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Finset.SupIndep` `Submodule` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `instOrderBot` `torsionBySet` `setLike`	—	`disjoint_iff` `Finset.sup_eq_iSup` `iSup_torsionBySet_ideal_eq_torsionBySet_iInf` `GaloisConnection.u_inf` `torsion_gc` `Ideal.sup_iInf_eq_top` `Ideal.instIsTwoSided` `top_coe` `torsionBySet_univ`
`torsion'_isTorsion'` 📖	mathematical	—	`Module.IsTorsion'` `Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `torsion'` `addCommMonoid` `instSMulSubtypeMemTorsion'`	—	—
`torsion'_torsion'_eq_top` 📖	mathematical	—	`torsion'` `Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `instDistribMulActionSubtypeMemTorsion'` `instSMulCommClassSubtypeMemTorsion'` `Top.top` `instTop`	—	`instSMulCommClassSubtypeMemTorsion'` `isTorsion'_iff_torsion'_eq_top` `torsion'_isTorsion'`
`torsionBySet_eq_torsionBySet_span` 📖	mathematical	—	`torsionBySet` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.span`	—	`le_antisymm` `mem_torsionBySet_iff` `Ideal.span_le` `torsionBySet_le_torsionBySet_of_subset` `subset_span`
`torsionBySet_isInternal` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `idemSemiring` `Algebra.id` `Top.top` `instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Module.IsTorsionBySet` `AddCommGroup.toAddCommMonoid` `setLike` `iInf` `instInfSet` `Finset.instMembership`	`DirectSum.IsInternal` `SetLike.instMembership` `Submodule` `addSubmonoidClass` `torsionBySet`	—	`DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top` `iSupIndep_iff_supIndep` `supIndep_torsionBySet_ideal` `iSup_subtype''` `iSup_torsionBySet_ideal_eq_torsionBySet_iInf` `Module.isTorsionBySet_iff_torsionBySet_eq_top`
`torsionBySet_isTorsionBySet` 📖	mathematical	—	`Module.IsTorsionBySet` `Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `torsionBySet` `addCommMonoid` `module`	—	`mem_torsionBySet_iff`
`torsionBySet_le_torsionBySet_of_subset` 📖	mathematical	`Set` `Set.instHasSubset`	`Submodule` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `torsionBySet`	—	`sInf_le_sInf`
`torsionBySet_singleton_eq` 📖	mathematical	—	`torsionBySet` `Set` `Set.instSingletonSet` `torsionBy`	—	`ext`
`torsionBySet_span_singleton_eq` 📖	mathematical	—	`torsionBySet` `SetLike.coe` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `setLike` `span` `Set` `Set.instSingletonSet` `torsionBy`	—	`torsionBySet_eq_torsionBySet_span` `torsionBySet_singleton_eq`
`torsionBySet_torsionBySet_eq_top` 📖	mathematical	—	`torsionBySet` `Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `Top.top` `instTop`	—	`Module.isTorsionBySet_iff_torsionBySet_eq_top` `torsionBySet_isTorsionBySet`
`torsionBySet_univ` 📖	mathematical	—	`torsionBySet` `Set.univ` `Bot.bot` `Submodule` `CommSemiring.toSemiring` `instBot`	—	`eq_bot_iff` `torsionBy_one` `torsionBySet_singleton_eq` `torsionBySet_le_torsionBySet_of_subset`
`torsionBy_isInternal` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.onFun` `IsCoprime` `CommRing.toCommSemiring` `Module.IsTorsionBy` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `Finset.prod` `CommRing.toCommMonoid`	`DirectSum.IsInternal` `SetLike.instMembership` `Submodule` `setLike` `addSubmonoidClass` `torsionBy`	—	`addSubmonoidClass` `torsionBySet_span_singleton_eq` `torsionBySet_isInternal` `Ideal.sup_eq_top_iff_isCoprime` `Finset.inf_eq_iInf` `Ideal.finset_inf_span_singleton` `Ideal.submodule_span_eq` `Module.isTorsionBySet_span_singleton_iff`
`torsionBy_isTorsionBy` 📖	mathematical	—	`Module.IsTorsionBy` `Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `torsionBy` `addCommMonoid` `module`	—	`smul_torsionBy`
`torsionBy_le_torsionBy_of_dvd` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring`	`Submodule` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `torsionBy`	—	`torsionBySet_span_singleton_eq` `torsionBySet_singleton_eq` `torsionBySet_le_torsionBySet_of_subset` `Ideal.mem_span_singleton`
`torsionBy_one` 📖	mathematical	—	`torsionBy` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Bot.bot` `Submodule` `instBot`	—	`eq_bot_iff` `one_smul` `mem_torsionBy_iff`
`torsionBy_torsionBy_eq_top` 📖	mathematical	—	`torsionBy` `Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `Top.top` `instTop`	—	`Module.isTorsionBy_iff_torsionBy_eq_top` `torsionBy_isTorsionBy`
`torsion_gc` 📖	mathematical	—	`GaloisConnection` `Submodule` `CommSemiring.toSemiring` `OrderDual` `Ideal` `PartialOrder.toPreorder` `instPartialOrder` `OrderDual.instPreorder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `annihilator` `torsionBySet` `SetLike.coe` `setLike` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	`mem_torsionBySet_iff` `mem_annihilator`
`torsion_int` 📖	mathematical	—	`toAddSubgroup` `Int.instRing` `AddCommGroup.toIntModule` `torsion` `Int.instCommSemiring` `AddCommGroup.toAddCommMonoid` `AddCommGroup.torsion`	—	`AddSubgroup.ext` `isOfFinAddOrder_iff_zsmul_eq_zero` `IsStrictOrderedRing.noZeroDivisors` `Int.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Int.instNontrivial`
`torsion_isTorsion` 📖	mathematical	—	`Module.IsTorsion` `Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `torsion` `addCommMonoid` `module`	—	`torsion'_isTorsion'`
`torsion_torsion_eq_top` 📖	mathematical	—	`torsion` `Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `Top.top` `instTop`	—	`torsion'_torsion'_eq_top`

Submodule.QuotientTorsion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsTorsionFree` 📖	mathematical	—	`Module.IsTorsionFree` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `CommRing.toRing` `Submodule.torsion` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	—	`Submodule.isTorsionFree_iff_torsion_eq_bot` `torsion_eq_bot`
`torsion_eq_bot` 📖	mathematical	—	`Submodule.torsion` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `CommRing.toRing` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Bot.bot` `Submodule.instBot`	—	`eq_bot_iff` `Quotient.inductionOn'` `Submodule.mem_bot` `Submodule.Quotient.mk_eq_zero` `Submonoid.isScalarTower` `IsScalarTower.left` `Submodule.Quotient.mk_smul` `SubmonoidClass.toMulMemClass` `Submonoid.instSubmonoidClass` `SemigroupAction.mul_smul`

Submodule.torsionBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_ideal_smul` 📖	mathematical	—	`HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.torsionBy` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Submodule.addCommGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ideal.Quotient.semiring` `Module.toDistribMulAction` `Submodule.addCommMonoid` `Submodule.instModuleQuotientIdealSpanSingletonSetSubtypeMemTorsionBy` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `Submodule.smul` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid`	—	`Ideal.instIsTwoSided_1`
`mk_smul` 📖	mathematical	—	`HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Set` `Set.instSingletonSet` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.torsionBy` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Submodule.addCommGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ideal.Quotient.semiring` `Module.toDistribMulAction` `Submodule.addCommMonoid` `Submodule.instModuleQuotientTorsionBy` `DFunLike.coe` `RingHom` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `Submodule.smul` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid`	—	`Ideal.instIsTwoSided_1`

Submodule.torsionBySet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_smul` 📖	mathematical	—	`HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.torsionBySet` `SetLike.coe` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Submodule.addCommGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ideal.Quotient.semiring` `Module.toDistribMulAction` `Submodule.addCommMonoid` `Submodule.instModuleQuotientIdealSubtypeMemTorsionBySetCoe` `DFunLike.coe` `RingHom` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `Submodule.smul` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid`	—	`Ideal.instIsTwoSided_1`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`infinite_range_add_nsmul_iff` 📖	mathematical	—	`Set.Infinite` `Set.range` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`nsmul_zero` `add_zero` `Set.range_const` `Set.infinite_range_of_injective` `instInfiniteNat` `Int.instCharZero` `smul_left_injective` `Int.instIsCancelMulZero` `instIsTorsionFreeIntOfIsAddTorsionFree` `natCast_zsmul` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`infinite_range_add_smul_iff` 📖	mathematical	—	`Set.Infinite` `Set.range` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction`	—	`smul_zero` `add_zero` `Set.range_const` `Nontrivial.to_nonempty` `IsDomain.toNontrivial` `Set.infinite_range_of_injective` `smul_left_injective` `IsDomain.toIsCancelMulZero` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`isSMulRegular_iff_torsionBy_eq_bot` 📖	mathematical	—	`IsSMulRegular` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Submodule.torsionBy` `Bot.bot` `Submodule` `Submodule.instBot`	—	`smulCommClass_self` `LinearMap.ker_eq_bot`

---

← Back to Index