Documentation Verification Report

Pointwise

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

Statistics

Metric	Count
Definitions	0
Theorems `preimage_vadd_set`, `preimage_vadd_setₛₗ`, `preimage_vadd_setₛₗ`, `preimage_smul_set`, `preimage_smul_setₛₗ`, `preimage_vadd_set`, `preimage_vadd_setₛₗ`, `preimage_smul_set`, `preimage_smul_setₛₗ`, `preimage_smul_setₛₗ`, `smul_set`, `smul_setₛₗ`, `vadd_set`, `vadd_setₛₗ`, `image_smul_set`, `image_smul_setₛₗ`, `image_vadd_set`, `image_vadd_setₛₗ`, `preimage_smul_setₛₗ'`, `preimage_smul_setₛₗ_of_isUnit_isUnit`, `preimage_vadd_setₛₗ'`, `preimage_vadd_setₛₗ_of_isAddUnit_isAddUnit`, `smul_preimage_set_subset`, `smul_preimage_set_subsetₛₗ`, `vadd_preimage_set_subset`, `vadd_preimage_set_subsetₛₗ`	26
Total	26

AddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preimage_vadd_set` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`IsAddUnit.preimage_vadd_set` `isAddUnit`
`preimage_vadd_setₛₗ` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`preimage_vadd_setₛₗ_of_isAddUnit_isAddUnit` `isAddUnit`

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preimage_vadd_setₛₗ` 📖	mathematical	`IsAddUnit`	`Set.preimage` `DFunLike.coe` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instFunLike`	—	`IsAddUnit.preimage_vadd_setₛₗ` `instAddMonoidHomClass`

Group

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preimage_smul_set` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `toDivInvMonoid` `MulAction.toSemigroupAction`	—	`IsUnit.preimage_smul_set` `isUnit`
`preimage_smul_setₛₗ` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `toDivInvMonoid` `MulAction.toSemigroupAction`	—	`preimage_smul_setₛₗ_of_isUnit_isUnit` `isUnit`

IsAddUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preimage_vadd_set` 📖	mathematical	`IsAddUnit`	`Set.preimage` `DFunLike.coe` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction`	—	`preimage_vadd_setₛₗ_of_isAddUnit_isAddUnit`
`preimage_vadd_setₛₗ` 📖	mathematical	`IsAddUnit`	`Set.preimage` `DFunLike.coe` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction`	—	`preimage_vadd_setₛₗ_of_isAddUnit_isAddUnit` `map`

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preimage_smul_set` 📖	mathematical	`IsUnit`	`Set.preimage` `DFunLike.coe` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`preimage_smul_setₛₗ_of_isUnit_isUnit`
`preimage_smul_setₛₗ` 📖	mathematical	`IsUnit`	`Set.preimage` `DFunLike.coe` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`preimage_smul_setₛₗ_of_isUnit_isUnit` `map`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preimage_smul_setₛₗ` 📖	mathematical	`IsUnit`	`Set.preimage` `DFunLike.coe` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instFunLike`	—	`IsUnit.preimage_smul_setₛₗ` `instMonoidHomClass`

Set.MapsTo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_set` 📖	mathematical	`Set.MapsTo` `DFunLike.coe`	`Set` `Set.smulSet`	—	`smul_setₛₗ`
`smul_setₛₗ` 📖	mathematical	`Set.MapsTo` `DFunLike.coe`	`Set` `Set.smulSet`	—	`Function.Semiconj.mapsTo_image_right` `MulActionSemiHomClass.map_smulₛₗ`
`vadd_set` 📖	mathematical	`Set.MapsTo` `DFunLike.coe`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet`	—	`vadd_setₛₗ`
`vadd_setₛₗ` 📖	mathematical	`Set.MapsTo` `DFunLike.coe`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet`	—	`Function.Semiconj.mapsTo_image_right` `AddActionSemiHomClass.map_vaddₛₗ`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_smul_set` 📖	mathematical	—	`Set.image` `DFunLike.coe` `Set` `Set.smulSet`	—	`image_smul_setₛₗ`
`image_smul_setₛₗ` 📖	mathematical	—	`Set.image` `DFunLike.coe` `Set` `Set.smulSet`	—	`Function.Semiconj.set_image` `MulActionSemiHomClass.map_smulₛₗ`
`image_vadd_set` 📖	mathematical	—	`Set.image` `DFunLike.coe` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet`	—	`image_vadd_setₛₗ`
`image_vadd_setₛₗ` 📖	mathematical	—	`Set.image` `DFunLike.coe` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet`	—	`Function.Semiconj.set_image` `AddActionSemiHomClass.map_vaddₛₗ`
`preimage_smul_setₛₗ'` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `Set` `Set.smulSet`	—	`Set.Subset.antisymm` `Set.subset_def` `Function.Surjective.forall` `Set.smul_mem_smul_set` `MulActionSemiHomClass.map_smulₛₗ` `smul_preimage_set_subsetₛₗ`
`preimage_smul_setₛₗ_of_isUnit_isUnit` 📖	mathematical	`IsUnit`	`Set.preimage` `DFunLike.coe` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`preimage_smul_setₛₗ'` `Function.Bijective.surjective` `IsUnit.smul_bijective` `Function.Bijective.injective`
`preimage_vadd_setₛₗ'` 📖	mathematical	`HVAdd.hVAdd` `instHVAdd`	`Set.preimage` `DFunLike.coe` `Set` `Set.vaddSet`	—	`Set.Subset.antisymm` `Set.subset_def` `Function.Surjective.forall` `Set.vadd_mem_vadd_set` `AddActionSemiHomClass.map_vaddₛₗ` `vadd_preimage_set_subsetₛₗ`
`preimage_vadd_setₛₗ_of_isAddUnit_isAddUnit` 📖	mathematical	`IsAddUnit`	`Set.preimage` `DFunLike.coe` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction`	—	`preimage_vadd_setₛₗ'` `Function.Bijective.surjective` `IsAddUnit.vadd_bijective` `Function.Bijective.injective`
`smul_preimage_set_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.smulSet` `Set.preimage` `DFunLike.coe`	—	`smul_preimage_set_subsetₛₗ`
`smul_preimage_set_subsetₛₗ` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.smulSet` `Set.preimage` `DFunLike.coe`	—	`Set.MapsTo.subset_preimage` `Set.MapsTo.smul_setₛₗ` `Set.mapsTo_preimage`
`vadd_preimage_set_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `Set.preimage` `DFunLike.coe`	—	`vadd_preimage_set_subsetₛₗ`
`vadd_preimage_set_subsetₛₗ` 📖	mathematical	—	`Set` `Set.instHasSubset` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `Set.preimage` `DFunLike.coe`	—	`Set.MapsTo.subset_preimage` `Set.MapsTo.vadd_setₛₗ` `Set.mapsTo_preimage`

---

← Back to Index