Theorems · Theorem · group theory

Subgroup.equivSMul_symm_apply_coe

∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Group α] [inst_2 : MulDistribMulAction α G] (a : α)
  (H : Subgroup G) (y : ↑(⇑↑(MulDistribMulAction.toMulEquiv G a) '' ↑H.toSubmonoid)),
  ↑((Subgroup.equivSMul a H).symm y) = a⁻¹ • ↑y

Defined in

Mathlib.Algebra.Group.Subgroup.Pointwise

Cited by

0 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupGroupMulDistribMulAction