instMulAction_1 — Mathlib

English

The proof that the defined action respects the group operation on the left, establishing a genuine action.

Русский

Доказано, что данное действие согласуется с операцией группы слева, образуя действительное действие.

LaTeX

$$$\\text{proof of } \\text{instMulAction}_1: \\forall a,b, (a b)\\cdot w = a\\cdot (b\\cdot w).$$$

Lean4

noncomputable instance : MulAction (HNNExtension G A B φ) (NormalWord d) :=
  MulAction.ofEndHom <|
    (MulAction.toEndHom (M := Equiv.Perm (NormalWord d))).comp
      (HNNExtension.lift (MulAction.toPermHom _ _) (unitsSMulEquiv φ) <|
        by
        intro a
        ext : 1
        simp [unitsSMul_one_group_smul])

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