Pointwise

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

Statistics

Metric	Count
Definitions `hasDistribNeg`, `monoid`, `mul`, `mulOneClass`, `one`, `semigroup`, `smul`	7
Theorems `addSubmonoid_smul_bot`, `addSubmonoid_smul_sup`, `bot_mul`, `closure_mul_closure`, `closure_pow`, `iSup_mul`, `mem_one`, `mul_bot`, `mul_comm_of_commute`, `mul_eq_closure_mul_set`, `mul_iSup`, `mul_induction_on`, `mul_le`, `mul_le_mul`, `mul_le_mul_left`, `mul_le_mul_right`, `mul_mem_mul`, `mul_subset_mul`, `mul_sup`, `natCast_mem_one`, `one_eq_closure`, `one_eq_closure_one_set`, `one_eq_mrange`, `pow_eq_closure_pow_set`, `pow_subset_pow`, `smul_iSup`, `smul_induction_on`, `smul_le`, `smul_le_smul`, `smul_le_smul_left`, `smul_le_smul_right`, `smul_mem_smul`, `smul_subset_smul`, `sup_mul`	34
Total	41

AddSubmonoid

Definitions

Name	Category	Theorems
`hasDistribNeg` 📖	CompOp	—
`monoid` 📖	CompOp	5 math math: `pow_eq_closure_pow_set`, `pow_subset_pow`, `closure_pow`, `Submodule.pow_toAddSubmonoid`, `Submodule.le_pow_toAddSubmonoid`
`mul` 📖	CompOp	17 math math: `mul_le_mul_left`, `sup_mul`, `mul_iSup`, `mul_sup`, `Submodule.mul_toAddSubmonoid`, `AddSubgroup.mul_toAddSubmonoid`, `mul_le`, `mul_subset_mul`, `mul_comm_of_commute`, `mul_le_mul`, `mul_le_mul_right`, `bot_mul`, `mul_mem_mul`, `mul_bot`, `iSup_mul`, `closure_mul_closure`, `mul_eq_closure_mul_set`
`mulOneClass` 📖	CompOp	—
`one` 📖	CompOp	6 math math: `mem_one`, `natCast_mem_one`, `Submodule.le_one_toAddSubmonoid`, `one_eq_mrange`, `one_eq_closure`, `one_eq_closure_one_set`
`semigroup` 📖	CompOp	—
`smul` 📖	CompOp	10 math math: `smul_iSup`, `smul_mem_smul`, `smul_le`, `smul_le_smul`, `Submodule.smul_toAddSubmonoid`, `smul_subset_smul`, `smul_le_smul_left`, `addSubmonoid_smul_sup`, `addSubmonoid_smul_bot`, `smul_le_smul_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addSubmonoid_smul_bot` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `smul` `Bot.bot` `instBot`	—	`eq_bot_iff` `smul_le` `mem_bot` `smul_zero`
`addSubmonoid_smul_sup` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `smul` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`le_antisymm` `smul_le` `closure_induction` `le_sup_left` `smul_mem_smul` `le_sup_right` `zero_mem` `smul_zero` `smul_add` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `instAddSubmonoidClass` `sup_eq_closure` `sup_le` `smul_le_smul_right`
`bot_mul` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `mul` `Bot.bot` `instBot`	—	`eq_bot_iff` `mul_le` `mem_bot` `MulZeroClass.zero_mul`
`closure_mul_closure` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `mul` `closure` `Set` `Set.mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`le_antisymm` `mul_le` `AddMonoidHom.mulRight_apply` `AddMonoidHom.instAddMonoidHomClass` `mem_comap` `closure_le` `subset_closure` `Set.mul_mem_mul` `mul_mem_mul`
`closure_pow` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `monoid` `closure` `Set` `Set.NPow` `AddMonoidWithOne.toOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`pow_zero` `one_eq_closure_one_set` `pow_succ` `closure_mul_closure`
`iSup_mul` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `mul` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`le_antisymm` `mul_le` `iSup_induction` `mem_iSup_of_mem` `mul_mem_mul` `MulZeroClass.zero_mul` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `instAddSubmonoidClass` `right_distrib` `Distrib.rightDistribClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `iSup_le` `mul_le_mul_left` `le_iSup`
`mem_one` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `SetLike.instMembership` `instSetLike` `one` `AddMonoidWithOne.toNatCast`	—	—
`mul_bot` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `mul` `Bot.bot` `instBot`	—	`addSubmonoid_smul_bot`
`mul_comm_of_commute` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `mul`	—	`le_antisymm` `mul_le` `mul_mem_mul`
`mul_eq_closure_mul_set` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `mul` `closure` `Set` `Set.mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `SetLike.coe` `instSetLike`	—	`closure_mul_closure` `closure_eq`
`mul_iSup` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `mul` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`smul_iSup`
`mul_induction_on` 📖	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SetLike.instMembership` `instSetLike` `mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toAdd`	—	—	`smul_induction_on`
`mul_le` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `mul` `SetLike.instMembership` `instSetLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`smul_le`
`mul_le_mul` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`mul`	—	`smul_le_smul`
`mul_le_mul_left` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`mul`	—	`smul_le_smul_left`
`mul_le_mul_right` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`mul`	—	`smul_le_smul_right`
`mul_mem_mul` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SetLike.instMembership` `instSetLike`	`mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`smul_mem_smul`
`mul_subset_mul` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `SetLike.coe` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instSetLike` `mul`	—	`smul_subset_smul`
`mul_sup` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `mul` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`addSubmonoid_smul_sup`
`natCast_mem_one` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `SetLike.instMembership` `instSetLike` `one` `AddMonoidWithOne.toNatCast`	—	—
`one_eq_closure` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `one` `closure` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toOne`	—	`AddMonoidHom.instAddMonoidHomClass` `closure_singleton_eq` `one_eq_mrange` `AddMonoidHom.ext_nat` `Nat.cast_one` `nsmul_one`
`one_eq_closure_one_set` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `one` `closure` `Set` `Set.one` `AddMonoidWithOne.toOne`	—	`one_eq_closure`
`one_eq_mrange` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `one` `AddMonoidHom.mrange` `Nat.instAddMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `AddMonoidHom.instAddMonoidHomClass` `Nat.castAddMonoidHom`	—	—
`pow_eq_closure_pow_set` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `monoid` `closure` `Set` `Set.NPow` `AddMonoidWithOne.toOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `SetLike.coe` `instSetLike`	—	`closure_pow` `closure_eq`
`pow_subset_pow` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.NPow` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `SetLike.coe` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instSetLike` `Monoid.toNatPow` `monoid`	—	`subset_closure` `pow_eq_closure_pow_set`
`smul_iSup` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `smul` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`le_antisymm` `smul_le` `iSup_induction` `mem_iSup_of_mem` `smul_mem_smul` `smul_zero` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `instAddSubmonoidClass` `smul_add` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `iSup_le` `smul_le_smul_right` `le_iSup`
`smul_induction_on` 📖	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `DistribSMul.toSMulZeroClass` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	—	`smul_zero` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `instAddSubmonoidClass` `smul_le`
`smul_le` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `smul` `SetLike.instMembership` `instSetLike` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `DistribSMul.toSMulZeroClass`	—	`smul_mem_smul` `iSup_le` `map_le_iff_le_comap`
`smul_le_smul` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`smul`	—	`smul_le` `smul_mem_smul`
`smul_le_smul_left` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`smul`	—	`smul_le_smul` `le_rfl`
`smul_le_smul_right` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`smul`	—	`smul_le_smul` `le_rfl`
`smul_mem_smul` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike`	`smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `DistribSMul.toSMulZeroClass`	—	`le_iSup`
`smul_subset_smul` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `SetLike.coe` `AddSubmonoid` `instSetLike` `smul`	—	`Set.smul_subset_iff` `smul_mem_smul`
`sup_mul` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `mul` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`le_antisymm` `mul_le` `mem_sup` `right_distrib` `Distrib.rightDistribClass` `add_mem_sup` `mul_mem_mul` `sup_le` `mul_le_mul_left` `le_sup_left` `le_sup_right`

---

← Back to Index