IsSMulRegular

📁 Source: Mathlib/RingTheory/Regular/IsSMulRegular.lean

Statistics

Metric	Count
Definitions IsSMulRegular	1
Theorems isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, lTensor, rTensor, submodule, isSMulRegular_congr, isSMulRegular_congr', map_first_exact_on_four_term_exact_of_isSMulRegular_last, biUnion_associatedPrimes_eq_compl_regular, isSMulRegular_iff_ker_lsmul_eq_bot, isSMulRegular_of_isSMulRegular_on_submodule_on_quotient, isSMulRegular_of_ker_lsmul_eq_bot, isSMulRegular_of_range_eq_ker, isSMulRegular_on_quot_iff_lsmul_comap_eq, isSMulRegular_on_quot_iff_lsmul_comap_le, isSMulRegular_on_submodule_iff_disjoint_ker_lsmul_submodule, isSMulRegular_quotient_iff_mem_of_smul_mem, isSMulRegular_submodule_iff_right_eq_zero_of_smul, mem_of_isSMulRegular_quotient_of_smul_mem, smul_top_inf_eq_smul_of_isSMulRegular_on_quot	19
Total	20

IsSMulRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSMulRegular_on_quot_iff_smul_top_inf_eq_smul 📖	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	HasQuotient.Quotient Submodule Submodule.hasQuotient CommRing.toRing Submodule.Quotient.instSMul Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.instMin AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid Submodule.pointwiseDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring Top.top Submodule.instTop	—	smulCommClass_self isSMulRegular_on_quot_iff_lsmul_comap_le RingHomSurjective.ids Submodule.map_le_map_iff_of_injective LinearMap.lsmul_eq_distribSMultoLinearMap Submodule.map_comap_eq LinearMap.range_eq_map
lTensor 📖	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	TensorProduct TensorProduct.instSMul	—	smulCommClass_self TensorProduct.smulCommClass_left LinearMap.lTensor_smul_action Module.Flat.lTensor_preserves_injective_linearMap
rTensor 📖	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	TensorProduct TensorProduct.instSMul	—	smulCommClass_self TensorProduct.smulCommClass_left LinearMap.rTensor_smul_action Module.Flat.rTensor_preserves_injective_linearMap
submodule 📖	mathematical	IsSMulRegular SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Submodule SetLike.instMembership Submodule.setLike Submodule.smul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instDistribSMul NonAssocSemiring.toNonUnitalNonAssocSemiring IsScalarTower.left DistribMulAction.toMulAction	—	of_injective SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass Submodule.injective_subtype

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSMulRegular_congr 📖	mathematical	—	IsSMulRegular SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	RingHomInvPair.ids isSMulRegular_congr'
isSMulRegular_congr' 📖	mathematical	—	IsSMulRegular SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	Equiv.isSMulRegular_congr LinearMap.map_smul'

QuotSMulTop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_first_exact_on_four_term_exact_of_isSMulRegular_last 📖	mathematical	Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid IsSMulRegular SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	QuotSMulTop Submodule.Quotient.addCommGroup CommRing.toRing Submodule AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid Submodule.pointwiseDistribMulAction Top.top Submodule.instTop Submodule.Quotient.module LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring Submodule.Quotient.smulCommClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction map Submodule.Quotient.instZeroQuotient	—	RingHomSurjective.ids IsSMulRegular.of_injective SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass le_of_eq Function.Exact.linearMap_ker_eq LinearMap.ker_eq_bot Submodule.ker_liftQ_eq_bot' smulCommClass_self Submodule.Quotient.smulCommClass Function.Exact.exact_mapQ_iff Submodule.map_pointwise_smul Submodule.map_top inf_comm smul_top_inf_eq_smul_of_isSMulRegular_on_quot

(root)

Definitions

Name	Category	Theorems
IsSMulRegular 📖	MathDef	55 math math: IsSMulRegular.of_mul_eq_one, IsUnit.isSMulRegular, isSMulRegular_iff_mem_nonZeroSMulDivisors, RingTheory.Sequence.isWeaklyRegular_cons_iff', Equiv.isSMulRegular_congr, RingTheory.Sequence.isWeaklyRegular_cons_iff, Units.isSMulRegular, Prod.isSMulRegular_iff, Module.IsTorsionFree.isSMulRegular, RingTheory.Sequence.isRegular_cons_iff, IsSMulRegular.of_right_eq_zero_of_smul, biUnion_associatedPrimes_eq_compl_regular, RingTheory.Sequence.isWeaklyRegular_iff_Fin, isSMulRegular_submodule_iff_right_eq_zero_of_smul, IsLeftRegular.isSMulRegular, isSMulRegular_map, RingTheory.Sequence.isWeaklyRegular_singleton_iff, isSMulRegular_iff_torsionBy_eq_bot, IsRegular.isSMulRegular, RingTheory.Sequence.IsWeaklyRegular.regular_mod_prev, Module.Flat.isSMulRegular_of_isRegular, IsSMulRegular.zero, isSMulRegular_algebraMap_iff, isSMulRegular_quotient_iff_mem_of_smul_mem, IsSMulRegular.of_smul_eq_one, IsSMulRegular.pow_iff, IsSMulRegular.mul_and_mul_iff, Pi.isSMulRegular_iff, isSMulRegular_of_group, isSMulRegular_of_ker_lsmul_eq_bot, LinearEquiv.isSMulRegular_congr', isRightRegular_iff, IsSMulRegular.mul_iff, ULift.isSMulRegular_iff, LinearEquiv.isSMulRegular_congr, IsSMulRegular.natAbs_iff, IsSMulRegular.not_zero, IsSMulRegular.skewMonoidAlgebra_iff, IsSMulRegular.subsingleton_linearMap_iff, IsSMulRegular.not_zero_iff, isSMulRegular_on_quot_iff_lsmul_comap_eq, IsLeftRegular.matrix, IsSMulRegular.zero_iff_subsingleton, isSMulRegular_on_submodule_iff_disjoint_ker_lsmul_submodule, RingTheory.Sequence.isWeaklyRegular_iff, IsRightRegular.isSMulRegular, isSMulRegular_iff_ker_lsmul_eq_bot, IsSMulRegular.one, isSMulRegular_on_quot_iff_lsmul_comap_le, isLeftRegular_iff, isSMulRegular_iff_right_eq_zero_of_smul, RingTheory.Sequence.isRegular_cons_iff', IsSMulRegular.of_ne_zero, Module.Flat.isSMulRegular_of_nonZeroDivisors, IsLocalizedModule.injective_iff_isRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biUnion_associatedPrimes_eq_compl_regular 📖	mathematical	—	Set.iUnion Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership associatedPrimes AddCommGroup.toAddCommMonoid SetLike.coe Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Compl.compl Set.instCompl setOf IsSMulRegular SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	biUnion_associatedPrimes_eq_zero_divisors
isSMulRegular_iff_ker_lsmul_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 LinearMap.ker RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid LinearMap.instFunLike LinearMap.lsmul Bot.bot Submodule Submodule.instBot	—	isSMulRegular_iff_torsionBy_eq_bot
isSMulRegular_of_isSMulRegular_on_submodule_on_quotient 📖	—	IsSMulRegular Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike 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 HasQuotient.Quotient Submodule.hasQuotient Submodule.Quotient.instSMul	—	—	IsScalarTower.left isSMulRegular_of_range_eq_ker Submodule.injective_subtype RingHomSurjective.ids Submodule.range_subtype Submodule.ker_mkQ
isSMulRegular_of_ker_lsmul_eq_bot 📖	mathematical	LinearMap.ker CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike LinearMap.lsmul Bot.bot Submodule Submodule.instBot	IsSMulRegular SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	smulCommClass_self isSMulRegular_iff_ker_lsmul_eq_bot
isSMulRegular_of_range_eq_ker 📖	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LinearMap.range RingHomSurjective.ids LinearMap.ker IsSMulRegular SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—	RingHomSurjective.ids IsSMulRegular.of_right_eq_zero_of_smul IsSMulRegular.right_eq_zero_of_smul LinearMap.map_smul LinearMap.map_zero
isSMulRegular_on_quot_iff_lsmul_comap_eq 📖	mathematical	—	IsSMulRegular HasQuotient.Quotient Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient CommRing.toRing Submodule.Quotient.instSMul Submodule.comap RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike LinearMap.lsmul	—	smulCommClass_self isSMulRegular_on_quot_iff_lsmul_comap_le LE.le.ge_iff_eq' Submodule.smul_mem
isSMulRegular_on_quot_iff_lsmul_comap_le 📖	mathematical	—	IsSMulRegular HasQuotient.Quotient Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient CommRing.toRing Submodule.Quotient.instSMul Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.comap RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike LinearMap.lsmul	—	isSMulRegular_quotient_iff_mem_of_smul_mem
isSMulRegular_on_submodule_iff_disjoint_ker_lsmul_submodule 📖	mathematical	—	IsSMulRegular Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.smul Algebra.toSMul Algebra.id SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Disjoint Submodule.instPartialOrder Submodule.instOrderBot LinearMap.ker RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid CommMonoid.toMonoid LinearMap.instFunLike LinearMap.lsmul	—	IsScalarTower.left smulCommClass_self isSMulRegular_submodule_iff_right_eq_zero_of_smul disjoint_comm Submodule.disjoint_def
isSMulRegular_quotient_iff_mem_of_smul_mem 📖	mathematical	—	IsSMulRegular HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient Submodule.Quotient.instSMul SetLike.instMembership Submodule.setLike	—	isSMulRegular_iff_right_eq_zero_of_smul Function.Surjective.forall Submodule.mkQ_surjective SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass
isSMulRegular_submodule_iff_right_eq_zero_of_smul 📖	mathematical	—	IsSMulRegular Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike 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 NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	isSMulRegular_iff_right_eq_zero_of_smul SMulMemClass.smul_mem Submodule.smulMemClass
mem_of_isSMulRegular_quotient_of_smul_mem 📖	—	IsSMulRegular HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient Submodule.Quotient.instSMul 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 Module.toDistribMulAction	—	—	isSMulRegular_quotient_iff_mem_of_smul_mem
smul_top_inf_eq_smul_of_isSMulRegular_on_quot 📖	mathematical	IsSMulRegular HasQuotient.Quotient Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient CommRing.toRing Submodule.Quotient.instSMul	Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.instMin SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring Top.top Submodule.instTop	—	smulCommClass_self RingHomSurjective.ids Submodule.map_top Submodule.map_comap_eq Submodule.map_mono isSMulRegular_on_quot_iff_lsmul_comap_le

---

← Back to Index