Pointwise

📁 Source: Mathlib/Algebra/Ring/Subsemiring/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_toAddSubmonoid, smul_bot, smul_closure, smul_mem_pointwise_smul, smul_mem_pointwise_smul_iff, smul_mem_pointwise_smul_iff₀, smul_sup, subset_pointwise_smul_iff	22
Total	23

Subsemiring

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_pointwise_smul 📖	mathematical	—	SetLike.coe Subsemiring Semiring.toNonAssocSemiring instSetLike SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction Set Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction	—	—
instCovariantClassHSMulLe 📖	mathematical	—	CovariantClass Subsemiring Semiring.toNonAssocSemiring SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	Set.image_mono
le_pointwise_smul_iff₀ 📖	mathematical	—	Subsemiring Semiring.toNonAssocSemiring 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	—	Subsemiring Semiring.toNonAssocSemiring 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 AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction	—	Set.mem_inv_smul_set_iff
mem_inv_pointwise_smul_iff₀ 📖	mathematical	—	Subsemiring Semiring.toNonAssocSemiring 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 AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction	—	Set.mem_inv_smul_set_iff₀
mem_pointwise_smul_iff_inv_smul_mem 📖	mathematical	—	Subsemiring Semiring.toNonAssocSemiring SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Set.mem_smul_set_iff_inv_smul_mem
mem_pointwise_smul_iff_inv_smul_mem₀ 📖	mathematical	—	Subsemiring Semiring.toNonAssocSemiring SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	Set.mem_smul_set_iff_inv_smul_mem₀
mem_smul_pointwise_iff_exists 📖	mathematical	—	Subsemiring Semiring.toNonAssocSemiring SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction	—	Set.mem_smul_set
pointwise_central_scalar 📖	mathematical	—	IsCentralScalar Subsemiring Semiring.toNonAssocSemiring SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction MulOpposite MulOpposite.instMonoid	—	RingHom.ext IsCentralScalar.op_smul_eq_smul
pointwise_smul_def 📖	mathematical	—	Subsemiring Semiring.toNonAssocSemiring SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction map MulSemiringAction.toRingHom	—	—
pointwise_smul_le_iff₀ 📖	mathematical	—	Subsemiring Semiring.toNonAssocSemiring 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	—	Subsemiring Semiring.toNonAssocSemiring 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	—	Subsemiring Semiring.toNonAssocSemiring 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	—	Subsemiring Semiring.toNonAssocSemiring 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_toAddSubmonoid 📖	mathematical	—	toAddSubmonoid Semiring.toNonAssocSemiring Subsemiring SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction AddSubmonoid AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddSubmonoid.pointwiseMulAction MulSemiringAction.toDistribMulAction	—	—
smul_bot 📖	mathematical	—	Subsemiring Semiring.toNonAssocSemiring SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction Bot.bot instBot	—	map_bot
smul_closure 📖	mathematical	—	Subsemiring Semiring.toNonAssocSemiring SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction closure Set Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction	—	RingHom.map_closureS
smul_mem_pointwise_smul 📖	mathematical	Subsemiring Semiring.toNonAssocSemiring SetLike.instMembership instSetLike	SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction	—	Set.smul_mem_smul_set
smul_mem_pointwise_smul_iff 📖	mathematical	—	Subsemiring Semiring.toNonAssocSemiring SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction	—	Set.smul_mem_smul_set_iff
smul_mem_pointwise_smul_iff₀ 📖	mathematical	—	Subsemiring Semiring.toNonAssocSemiring SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction	—	Set.smul_mem_smul_set_iff₀
smul_sup 📖	mathematical	—	Subsemiring Semiring.toNonAssocSemiring SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	map_sup
subset_pointwise_smul_iff 📖	mathematical	—	Subsemiring Semiring.toNonAssocSemiring 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