mul_smul — Mathlib

English

In the context of GrpCat.SurjectiveOfEpiAuxs, the action satisfies (b b') • x = b • b' • x for all b,b' in B and x in X'.

Русский

В контексте GrpCat.SurjectiveOfEpiAuxs действие удовлетворяет (b b') • x = b • b' • x для всех b,b' ∈ B и x ∈ X'.

LaTeX

$$$ (b b') \cdot x = b \cdot (b' \cdot x) $$$

Lean4

theorem mul_smul (b b' : B) (x : X') : (b * b') • x = b • b' • x :=
  match x with
  | fromCoset y => by
    change fromCoset _ = fromCoset _
    simp only [leftCoset_assoc]
  | ∞ => rfl

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