equivSMul — Mathlib

English

There is a MulEquiv between a subgroup and its image under the action by a: an isomorphism H ≃* (a • H).

Русский

Существует мульти-эквивалентность между подгруппой и её образом при действии: H ≃* (a • H).

LaTeX

$$$ H \cong\!_* (a \cdot H) $$$

Lean4

/-- Applying a `MulDistribMulAction` results in an isomorphic subgroup -/
@[simps!]
def equivSMul (a : α) (H : Subgroup G) : H ≃* (a • H : Subgroup G) :=
  (MulDistribMulAction.toMulEquiv G a).subgroupMap H

Похожие утверждения