apply_weylGroup_smul — Mathlib

English

A technical lemma identifying the index‑to‑permutation correspondence used to prove range statements about WeylGroupToPerm.

Русский

Техническая лемма, устанавливающая соответствие индексов и перестановок, используемая для доказательства утверждений об образе WeylGroupToPerm.

LaTeX

$$$\\text{WeylGroupToPerm case analysis}$$$

Lean4

@[simp]
theorem apply_weylGroup_smul {B : P.InvariantForm} (g : P.weylGroup) (x y : M) : B.form (g • x) (g • y) = B.form x y :=
  by
  revert x y
  obtain ⟨g, hg⟩ := g
  induction hg using weylGroup.induction with
  | mem i => simp
  | one => simp
  | mul g₁ g₂ hg₁ hg₂ hg₁' hg₂' =>
    intro x y
    rw [← Submonoid.mk_mul_mk _ _ _ hg₁ hg₂, mul_smul, mul_smul, hg₁', hg₂']

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