Documentation Verification Report

Pointwise

📁 Source: Mathlib/Algebra/GroupWithZero/Submonoid/Pointwise.lean

Statistics

Metric	Count
Definitions `pointwiseMulAction`	1
Theorems `coe_pointwise_smul`, `le_pointwise_smul_iff`, `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_isCentralScalar`, `pointwise_smul_le_iff`, `pointwise_smul_le_iff₀`, `pointwise_smul_le_pointwise_smul_iff`, `pointwise_smul_le_pointwise_smul_iff₀`, `smul_bot`, `smul_closure`, `smul_mem_pointwise_smul`, `smul_mem_pointwise_smul_iff`, `smul_mem_pointwise_smul_iff₀`, `smul_sup`, `le_pointwise_smul_iff₀`, `mem_inv_pointwise_smul_iff₀`, `mem_pointwise_smul_iff_inv_smul_mem₀`, `pointwise_smul_le_iff₀`, `pointwise_smul_le_pointwise_smul_iff₀`, `smul_mem_pointwise_smul_iff₀`	25
Total	26

AddSubmonoid

Definitions

Name	Category	Theorems
`pointwiseMulAction` 📖	CompOp	23 math math: `pointwise_smul_le_pointwise_smul_iff₀`, `le_pointwise_smul_iff`, `smul_bot`, `smul_sup`, `Subsemiring.pointwise_smul_toAddSubmonoid`, `Submodule.pointwise_smul_toAddSubmonoid`, `mem_pointwise_smul_iff_inv_smul_mem`, `pointwise_isCentralScalar`, `smul_mem_pointwise_smul`, `pointwise_smul_le_iff`, `mem_inv_pointwise_smul_iff₀`, `smul_closure`, `AddSubgroup.pointwise_smul_toAddSubmonoid`, `mem_pointwise_smul_iff_inv_smul_mem₀`, `smul_mem_pointwise_smul_iff₀`, `mem_inv_pointwise_smul_iff`, `coe_pointwise_smul`, `smul_mem_pointwise_smul_iff`, `pointwise_smul_le_pointwise_smul_iff`, `le_pointwise_smul_iff₀`, `Ideal.pointwise_smul_toAddSubmonoid`, `mem_smul_pointwise_iff_exists`, `pointwise_smul_le_iff₀`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_pointwise_smul` 📖	mathematical	—	`SetLike.coe` `AddSubmonoid` `AddMonoid.toAddZeroClass` `instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `Set` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	—
`le_pointwise_smul_iff` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `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`
`le_pointwise_smul_iff₀` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `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	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `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` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`Set.mem_inv_smul_set_iff`
`mem_inv_pointwise_smul_iff₀` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `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` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`Set.mem_inv_smul_set_iff₀`
`mem_pointwise_smul_iff_inv_smul_mem` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `pointwiseMulAction` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Set.mem_smul_set_iff_inv_smul_mem`
`mem_pointwise_smul_iff_inv_smul_mem₀` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `pointwiseMulAction` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`Set.mem_smul_set_iff_inv_smul_mem₀`
`mem_smul_pointwise_iff_exists` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`Set.mem_smul_set`
`pointwise_isCentralScalar` 📖	mathematical	—	`IsCentralScalar` `AddSubmonoid` `AddMonoid.toAddZeroClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `MulOpposite` `MulOpposite.instMonoid`	—	`AddMonoid.End.instAddMonoidHomClass` `AddMonoidHom.ext` `IsCentralScalar.op_smul_eq_smul`
`pointwise_smul_le_iff` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `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_le_iff₀` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `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	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `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	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `pointwiseMulAction`	—	`Set.smul_set_subset_smul_set_iff₀`
`smul_bot` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `Bot.bot` `instBot`	—	`map_bot`
`smul_closure` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `closure` `Set` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`AddMonoidHom.map_mclosure`
`smul_mem_pointwise_smul` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`Set.smul_mem_smul_set`
`smul_mem_pointwise_smul_iff` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `pointwiseMulAction` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`Set.smul_mem_smul_set_iff`
`smul_mem_pointwise_smul_iff₀` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `pointwiseMulAction` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`Set.smul_mem_smul_set_iff₀`
`smul_sup` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `pointwiseMulAction` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`map_sup`

Submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_pointwise_smul_iff₀` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `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	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `pointwiseMulAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `MulDistribMulAction.toMulAction`	—	`Set.mem_inv_smul_set_iff₀`
`mem_pointwise_smul_iff_inv_smul_mem₀` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `pointwiseMulAction` `MulDistribMulAction.toMulAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`Set.mem_smul_set_iff_inv_smul_mem₀`
`pointwise_smul_le_iff₀` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `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	—	`Submonoid` `Monoid.toMulOneClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `pointwiseMulAction`	—	`Set.smul_set_subset_smul_set_iff₀`
`smul_mem_pointwise_smul_iff₀` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `pointwiseMulAction` `MulDistribMulAction.toMulAction`	—	`Set.smul_mem_smul_set_iff₀`

---

← Back to Index