g_apply_fromCoset — Mathlib

English

For x ∈ B and y ∈ X, g(x) acts on fromCoset(y) by sending it to fromCoset(x•y).

Русский

Для x ∈ B и y ∈ X, действие g(x) на fromCoset(y) отправляет в fromCoset(x•y).

LaTeX

$$$$ g(x)(\mathrm{fromCoset}(y)) = \mathrm{fromCoset}(x \cdot y). $$$$

Lean4

theorem g_apply_fromCoset (x : B) (y : X) :
    g x (fromCoset y) = fromCoset ⟨x • ↑y, by obtain ⟨z, hz⟩ := y.2; exact ⟨x * z, by simp [← hz, smul_smul]⟩⟩ :=
  rfl

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