mk_smul — Mathlib

English

For g ∈ G, hg ∈ S with h ∈ S, and a ∈ α, the action of the pair ⟨g, hg⟩ on a equals the action of g on a: ⟨g, hg⟩ • a = g • a.

Русский

Для g ∈ G, hg ∈ S и a ∈ α, действие пары ⟨g,hg⟩ на a равно действию g на a: ⟨g,hg⟩ • a = g • a.

LaTeX

$$$\langle g,hg \rangle \cdot a = g \cdot a$$$

Lean4

@[to_additive (attr := simp)]
theorem mk_smul (g : G) (hg : g ∈ S) (a : α) : (⟨g, hg⟩ : S) • a = g • a :=
  rfl

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