Structures · Algebra
MulActionSemiHomClass
MulActionSemiHomClass F φ X Y states that
F is a type of morphisms which are φ-equivariant.
You should extend this class when you extend MulActionHom.
- Defined in
- Mathlib.GroupTheory.GroupAction.Hom
- Shape
- 4 explicit arguments · adds map_smulₛₗ
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by4
Concrete types that are instances1
- MulActionHom
How is a type an instance?
Loading the hierarchy index…
Assumed by12
- MulActionSemiHomClass.map_smulₛₗ
- MulActionSemiHomClass.toMulActionHom
- continuousSMul_inducedₛₗ
- IsUnit.preimage_smul_setₛₗ
- preimage_smul_setₛₗ_of_isUnit_isUnit
- Set.MapsTo.smul_setₛₗ
- smul_preimage_set_subsetₛₗ
- image_smul_setₛₗ
- preimage_smul_setₛₗ'
- Group.preimage_smul_setₛₗ
- MonoidHom.preimage_smul_setₛₗ
- MulActionHom.instCoeTCOfMulActionSemiHomClass
Ancestors0
No ancestors.