Pointwise

📁 Source: Mathlib/RingTheory/Ideal/Pointwise.lean

Statistics

Metric	Count
Definitions inertiaEquiv, pointwiseDistribMulAction, pointwiseMulSemiringAction, stabilizerEquiv	4
Theorems smul, smul_iff, inertiaEquiv_apply_smul, inertiaEquiv_symm_apply_smul, inertia_le_stabilizer, instCovariantClassHSMulLe, instNormalSubtypeMemSubgroupStabilizerSubgroupOfInertia, mem_inv_pointwise_smul_iff, mem_pointwise_smul_iff_inv_smul_mem, pointwise_central_scalar, pointwise_smul_def, pointwise_smul_eq_comap, pointwise_smul_le_pointwise_smul_iff, pointwise_smul_subset_iff, pointwise_smul_toAddSubgroup, pointwise_smul_toAddSubmonoid, smul_bot, smul_closure, smul_mem_pointwise_smul, smul_mem_pointwise_smul_iff, smul_sup, stabilizerEquiv_apply_smul, stabilizerEquiv_symm_apply_smul, subset_pointwise_smul_iff	24
Total	28

Ideal

Definitions

Name	Category	Theorems
inertiaEquiv 📖	CompOp	2 math math: inertiaEquiv_apply_smul, inertiaEquiv_symm_apply_smul
pointwiseDistribMulAction 📖	CompOp	48 math math: Quotient.map_ker_stabilizer_subtype, relNorm_smul, smul_closure, mem_pointwise_smul_iff_inv_smul_mem, exists_smul_eq_of_isGaloisGroup, subset_pointwise_smul_iff, LiesOver.smul, smul_sup, Quotient.stabilizerHom_surjective, pointwise_smul_subset_iff, instCovariantClassHSMulLe, Algebra.IsInvariant.exists_smul_of_under_eq, under_smul, IsDecompositionField.toIsGaloisGroup, card_stabilizer_eq, stabilizerEquiv_symm_apply_smul, IsPrime.smul_iff, isDecompositionField_iff, Quotient.stabilizerHom_surjective_of_profinite, inertia_le_stabilizer, Algebra.IsInvariant.orbit_eq_primesOver, Quotient.stabilizerHomSurjectiveAuxFunctor_aux, IsFractionRing.stabilizerHom_surjective, Quotient.stabilizerHom_apply, Algebra.IsInvariant.exists_smul_of_under_eq_of_profinite, Quotient.stabilizerQuotientInertiaEquiv_mk, instIsDecompositionFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupStabilizerIdealOfIsGalois, coe_smul_primesOver_mk, IsCyclotomicExtension.Rat.galEquivZMod_stabilizer, pointwise_smul_eq_comap, IsPrime.smul, IsFractionRing.stabilizerHom_apply_apply_mk, smul_mem_pointwise_smul, Quotient.ker_stabilizerHom, smul_bot, pointwise_smul_le_pointwise_smul_iff, card_stabilizer_eq_card_inertia_mul_finrank, pointwise_central_scalar, pointwise_smul_toAddSubgroup, smul_mem_pointwise_smul_iff, coe_smul_primesOver, exists_map_eq_of_isGalois, instNormalSubtypeMemSubgroupStabilizerSubgroupOfInertia, IsArithFrobAt.conj, pointwise_smul_toAddSubmonoid, mem_inv_pointwise_smul_iff, pointwise_smul_def, stabilizerEquiv_apply_smul
pointwiseMulSemiringAction 📖	CompOp	—
stabilizerEquiv 📖	CompOp	2 math math: stabilizerEquiv_symm_apply_smul, stabilizerEquiv_apply_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inertiaEquiv_apply_smul 📖	mathematical	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid MulSemiringAction.toDistribMulAction Ring.toSemiring DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike	Subgroup SetLike.instMembership Subgroup.instSetLike inertia DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Ring.toSemiring MulSemiringAction.toDistribMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Subgroup.toGroup Subgroup.instDistribMulActionSubtypeMem DFunLike.coe MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike inertiaEquiv	—	—
inertiaEquiv_symm_apply_smul 📖	mathematical	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid MulSemiringAction.toDistribMulAction Ring.toSemiring DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike	Subgroup SetLike.instMembership Subgroup.instSetLike inertia DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Ring.toSemiring MulSemiringAction.toDistribMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Subgroup.toGroup Subgroup.instDistribMulActionSubtypeMem DFunLike.coe MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm inertiaEquiv	—	MulEquiv.apply_symm_apply inertiaEquiv_apply_smul
inertia_le_stabilizer 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder inertia DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Ring.toSemiring MulSemiringAction.toDistribMulAction MulAction.stabilizer Ideal Submodule.instAddCommMonoidWithOne Semiring.toModule pointwiseDistribMulAction	—	SetLike.ext mem_pointwise_smul_iff_inv_smul_mem add_mem_iff_left InvMemClass.inv_mem SubgroupClass.toInvMemClass Subgroup.instSubgroupClass add_sub_cancel
instCovariantClassHSMulLe 📖	mathematical	—	CovariantClass Ideal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	map_mono
instNormalSubtypeMemSubgroupStabilizerSubgroupOfInertia 📖	mathematical	—	Subgroup.Normal Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Ideal Ring.toSemiring DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule pointwiseDistribMulAction Subgroup.toGroup Subgroup.subgroupOf inertia NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction	—	Subgroup.normal_subgroupOf_iff inertia_le_stabilizer Submodule.mem_toAddSubgroup smul_mem_pointwise_smul_iff smul_sub smul_smul mul_assoc inv_mul_cancel_left SemigroupAction.mul_smul Subgroup.inv_mem
mem_inv_pointwise_smul_iff 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid pointwiseDistribMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid NonAssocSemiring.toAddCommMonoidWithOne MulSemiringAction.toDistribMulAction	—	mem_pointwise_smul_iff_inv_smul_mem inv_inv
mem_pointwise_smul_iff_inv_smul_mem 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid pointwiseDistribMulAction NonAssocSemiring.toAddCommMonoidWithOne MulSemiringAction.toDistribMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	inv_smul_smul smul_mem_pointwise_smul smul_inv_smul
pointwise_central_scalar 📖	mathematical	—	IsCentralScalar Ideal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction MulOpposite MulOpposite.instMonoid	—	RingHom.ext IsCentralScalar.op_smul_eq_smul
pointwise_smul_def 📖	mathematical	—	Ideal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MulSemiringAction.toRingHom	—	—
pointwise_smul_eq_comap 📖	mathematical	—	Ideal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid pointwiseDistribMulAction comap RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm DFunLike.coe MonoidHom RingAut MulOneClass.toMulOne Monoid.toMulOneClass RingAut.instGroup MonoidHom.instFunLike MulSemiringAction.toRingAut RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass	—	ext RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass comap_symm
pointwise_smul_le_pointwise_smul_iff 📖	mathematical	—	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid pointwiseDistribMulAction	—	inv_smul_smul smul_mono_right instCovariantClassHSMulLe
pointwise_smul_subset_iff 📖	mathematical	—	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid pointwiseDistribMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	pointwise_smul_le_pointwise_smul_iff inv_smul_smul
pointwise_smul_toAddSubgroup 📖	mathematical	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Ring.toSemiring	Submodule.toAddSubgroup Ring.toAddCommGroup Semiring.toModule Ring.toSemiring Ideal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction AddSubgroup AddCommGroup.toAddGroup SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction AddSubgroup.pointwiseMulAction MulSemiringAction.toDistribMulAction	—	AddSubgroup.ext mem_map_iff_of_surjective RingHom.instRingHomClass
pointwise_smul_toAddSubmonoid 📖	mathematical	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction	Submodule.toAddSubmonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction AddSubmonoid AddCommMonoid.toAddMonoid SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction AddSubmonoid.pointwiseMulAction NonAssocSemiring.toAddCommMonoidWithOne MulSemiringAction.toDistribMulAction	—	AddSubmonoid.ext mem_map_iff_of_surjective RingHom.instRingHomClass
smul_bot 📖	mathematical	—	Ideal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction Bot.bot Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	map_bot RingHom.instRingHomClass
smul_closure 📖	mathematical	—	Ideal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction span Set Set.smulSet NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction	—	map_span RingHom.instRingHomClass
smul_mem_pointwise_smul 📖	mathematical	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction NonAssocSemiring.toAddCommMonoidWithOne MulSemiringAction.toDistribMulAction	—	subset_span Set.smul_mem_smul_set
smul_mem_pointwise_smul_iff 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid pointwiseDistribMulAction NonAssocSemiring.toAddCommMonoidWithOne MulSemiringAction.toDistribMulAction	—	inv_smul_smul smul_mem_pointwise_smul
smul_sup 📖	mathematical	—	Ideal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	map_sup RingHom.instRingHomClass
stabilizerEquiv_apply_smul 📖	mathematical	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid MulSemiringAction.toDistribMulAction DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike	Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Ideal DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule pointwiseDistribMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Subgroup.toGroup Subgroup.instDistribMulActionSubtypeMem MulSemiringAction.toDistribMulAction DFunLike.coe MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike stabilizerEquiv	—	—
stabilizerEquiv_symm_apply_smul 📖	mathematical	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid MulSemiringAction.toDistribMulAction DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike	Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Ideal DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule pointwiseDistribMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Subgroup.toGroup Subgroup.instDistribMulActionSubtypeMem MulSemiringAction.toDistribMulAction DFunLike.coe MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm stabilizerEquiv	—	MulEquiv.apply_symm_apply stabilizerEquiv_apply_smul
subset_pointwise_smul_iff 📖	mathematical	—	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid pointwiseDistribMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	pointwise_smul_le_pointwise_smul_iff inv_smul_smul

Ideal.IsPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul 📖	mathematical	—	Ideal.IsPrime Ideal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid Ideal.pointwiseDistribMulAction	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass Ideal.pointwise_smul_eq_comap comap
smul_iff 📖	mathematical	—	Ideal.IsPrime Ideal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid Ideal.pointwiseDistribMulAction	—	smul inv_smul_smul

---

← Back to Index