Pointwise

📁 Source: Mathlib/Algebra/Ring/Subring/Pointwise.lean

Statistics

Metric	Count
Definitions pointwiseMulAction	1
Theorems coe_pointwise_smul, instCovariantClassHSMulLe, le_pointwise_smul_iff₀, mem_inv_pointwise_smul_iff, mem_inv_pointwise_smul_iff₀, mem_pointwise_smul_iff_inv_smul_mem, mem_pointwise_smul_iff_inv_smul_mem₀, mem_smul_pointwise_iff_exists, pointwise_central_scalar, pointwise_smul_def, pointwise_smul_le_iff₀, pointwise_smul_le_pointwise_smul_iff, pointwise_smul_le_pointwise_smul_iff₀, pointwise_smul_subset_iff, pointwise_smul_toAddSubgroup, pointwise_smul_toSubsemiring, smul_bot, smul_closure, smul_mem_pointwise_smul, smul_mem_pointwise_smul_iff, smul_mem_pointwise_smul_iff₀, smul_sup, subset_pointwise_smul_iff	23
Total	24

Subring

Definitions

Name	Category	Theorems
pointwiseMulAction 📖	CompOp	25 math math: pointwise_smul_def, mem_pointwise_smul_iff_inv_smul_mem, mem_pointwise_smul_iff_inv_smul_mem₀, pointwise_smul_toAddSubgroup, coe_pointwise_smul, mem_inv_pointwise_smul_iff, pointwise_smul_subset_iff, ValuationSubring.pointwise_smul_toSubring, mem_smul_pointwise_iff_exists, smul_bot, smul_closure, instCovariantClassHSMulLe, le_pointwise_smul_iff₀, smul_mem_pointwise_smul_iff₀, pointwise_central_scalar, pointwise_smul_le_pointwise_smul_iff, pointwise_smul_le_iff₀, pointwise_smul_le_pointwise_smul_iff₀, smul_sup, subset_pointwise_smul_iff, smul_mem_pointwise_smul, smul_mem_pointwise_smul_iff, pointwise_smul_toSubsemiring, Subalgebra.pointwise_smul_toSubring, mem_inv_pointwise_smul_iff₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_pointwise_smul 📖	mathematical	—	SetLike.coe Subring instSetLike SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction Set Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Ring.toSemiring	—	—
instCovariantClassHSMulLe 📖	mathematical	—	CovariantClass Subring SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	Set.image_mono
le_pointwise_smul_iff₀ 📖	mathematical	—	Subring Preorder.toLE PartialOrder.toPreorder instPartialOrder SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	Set.subset_smul_set_iff₀
mem_inv_pointwise_smul_iff 📖	mathematical	—	Subring SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction pointwiseMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Ring.toSemiring	—	Set.mem_inv_smul_set_iff
mem_inv_pointwise_smul_iff₀ 📖	mathematical	—	Subring SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Ring.toSemiring	—	Set.mem_inv_smul_set_iff₀
mem_pointwise_smul_iff_inv_smul_mem 📖	mathematical	—	Subring SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Ring.toSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Set.mem_smul_set_iff_inv_smul_mem
mem_pointwise_smul_iff_inv_smul_mem₀ 📖	mathematical	—	Subring SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Ring.toSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	Set.mem_smul_set_iff_inv_smul_mem₀
mem_smul_pointwise_iff_exists 📖	mathematical	—	Subring SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Ring.toSemiring	—	Set.mem_smul_set
pointwise_central_scalar 📖	mathematical	—	IsCentralScalar Subring SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction MulOpposite MulOpposite.instMonoid	—	RingHom.ext IsCentralScalar.op_smul_eq_smul
pointwise_smul_def 📖	mathematical	—	Subring SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction map MulSemiringAction.toRingHom Ring.toSemiring	—	—
pointwise_smul_le_iff₀ 📖	mathematical	—	Subring Preorder.toLE PartialOrder.toPreorder instPartialOrder SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	Set.smul_set_subset_iff₀
pointwise_smul_le_pointwise_smul_iff 📖	mathematical	—	Subring Preorder.toLE PartialOrder.toPreorder instPartialOrder SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction pointwiseMulAction	—	Set.smul_set_subset_smul_set_iff
pointwise_smul_le_pointwise_smul_iff₀ 📖	mathematical	—	Subring Preorder.toLE PartialOrder.toPreorder instPartialOrder SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction	—	Set.smul_set_subset_smul_set_iff₀
pointwise_smul_subset_iff 📖	mathematical	—	Subring Preorder.toLE PartialOrder.toPreorder instPartialOrder SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction pointwiseMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Set.smul_set_subset_iff_subset_inv_smul_set
pointwise_smul_toAddSubgroup 📖	mathematical	—	toAddSubgroup Subring SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddSubgroup.pointwiseMulAction MulSemiringAction.toDistribMulAction Ring.toSemiring	—	—
pointwise_smul_toSubsemiring 📖	mathematical	—	toSubsemiring Subring SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction Subsemiring Semiring.toNonAssocSemiring Ring.toSemiring Subsemiring.pointwiseMulAction	—	—
smul_bot 📖	mathematical	—	Subring SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction Bot.bot instBot	—	map_bot
smul_closure 📖	mathematical	—	Subring SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction closure Set Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Ring.toSemiring	—	RingHom.map_closure
smul_mem_pointwise_smul 📖	mathematical	Subring SetLike.instMembership instSetLike	SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Ring.toSemiring	—	Set.smul_mem_smul_set
smul_mem_pointwise_smul_iff 📖	mathematical	—	Subring SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Ring.toSemiring	—	Set.smul_mem_smul_set_iff
smul_mem_pointwise_smul_iff₀ 📖	mathematical	—	Subring SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Ring.toSemiring	—	Set.smul_mem_smul_set_iff₀
smul_sup 📖	mathematical	—	Subring SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	map_sup
subset_pointwise_smul_iff 📖	mathematical	—	Subring Preorder.toLE PartialOrder.toPreorder instPartialOrder SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction pointwiseMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Set.subset_smul_set_iff

---

← Back to Index