Theorems · Definition · group theory
Subgroup.pointwiseMulAction
{α : Type u_1} →
{G : Type u_2} → [inst : Group G] → [inst_1 : Monoid α] → [MulDistribMulAction α G] → MulAction α (Subgroup G)The action on a subgroup corresponding to applying the action to every element.
This is available as an instance in the Pointwise locale.
- Defined in
- Mathlib.Algebra.Group.Subgroup.Pointwise
- Cited by
- 66 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Groupstatement and proof · cited by 6,238
- Monoidstatement and proof · cited by 3,887
- Subgroupstatement and proof · cited by 3,593
- MulActionstatement · cited by 1,294
- MulDistribMulActionstatement and proof · cited by 120
Cited by74
Results whose statement or proof uses this declaration.
- ModularForm.translatestatement · cited by 6
- CuspForm.translatestatement · cited by 3
- Subgroup.Commensurable.commensurable_conjstatement · cited by 3
- Subgroup.mem_pointwise_smul_iff_inv_smul_memstatement · cited by 3
- Subgroup.relIndex_pointwise_smulstatement · cited by 2
- Subgroup.equivSMulstatement · cited by 2
- Subgroup.smul_mem_pointwise_smulstatement · cited by 2
- Subgroup.Normal.conjActstatement · cited by 2
- CongruenceSubgroup.exists_Gamma_le_conj'statement · cited by 2
- Subgroup.pointwise_smul_defstatement · cited by 2
- Subgroup.conj_smul_le_of_lestatement · cited by 2
- Subgroup.IsArithmetic.conjstatement · cited by 1