Documentation Verification Report

Pointwise

📁 Source: Mathlib/GroupTheory/GroupAction/SubMulAction/Pointwise.lean

Statistics

Metric	Count
Definitions `instMonoid`, `instMul`, `instMulOneClass`, `instOne`, `instSemigroup`	5
Theorems `coe_mul`, `coe_one`, `coe_pow`, `mem_mul`, `mem_one`, `subset_coe_one`, `subset_coe_pow`	7
Total	12

SubMulAction

Definitions

Name	Category	Theorems
`instMonoid` 📖	CompOp	2 math math: `subset_coe_pow`, `coe_pow`
`instMul` 📖	CompOp	2 math math: `mem_mul`, `coe_mul`
`instMulOneClass` 📖	CompOp	—
`instOne` 📖	CompOp	6 math math: `algebraMap_mem`, `mem_one`, `subset_coe_one`, `coe_one`, `mem_one'`, `Submodule.toSubMulAction_one`
`instSemigroup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mul` 📖	mathematical	—	`SetLike.coe` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `instSetLike` `instMul` `Set` `Set.mul`	—	—
`coe_one` 📖	mathematical	—	`SetLike.coe` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `instSetLike` `instOne` `Set.range`	—	—
`coe_pow` 📖	mathematical	—	`SetLike.coe` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `instSetLike` `Monoid.toNatPow` `instMonoid` `Set` `Set.NPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toMul`	—	`pow_one` `pow_succ` `coe_mul`
`mem_mul` 📖	mathematical	—	`SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `SetLike.instMembership` `instSetLike` `instMul`	—	`Set.mem_mul`
`mem_one` 📖	mathematical	—	`SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `SetLike.instMembership` `instSetLike` `instOne`	—	—
`subset_coe_one` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.one` `SetLike.coe` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `instSetLike` `instOne`	—	`one_smul`
`subset_coe_pow` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.NPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toMul` `SetLike.coe` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `instSetLike` `Monoid.toNatPow` `instMonoid`	—	`pow_zero` `subset_coe_one` `coe_pow` `subset_refl` `Set.instReflSubset`

---

← Back to Index