rootForm_reflection_reflection_apply

English

RootForm is invariant under reflections: applying a reflection to both arguments leaves RootForm unchanged: RootForm(P.reflection i x, P.reflection i y) = RootForm(x,y).

Русский

RootForm инвариантна по отношению к отражениям: применение отражения к обоим аргументам не изменяет RootForm: RootForm(P.reflection i x, P.reflection i y) = RootForm(x,y).

LaTeX

$$$ P.RootForm(P.reflection(i,x), P.reflection(i,y)) = P.RootForm(x,y) $$$

Lean4

@[simp]
theorem rootForm_reflection_reflection_apply (i : ι) (x y : M) :
    P.RootForm (P.reflection i x) (P.reflection i y) = P.RootForm x y :=
  by
  simp only [rootForm_apply_apply, coroot'_reflection]
  exact
    Fintype.sum_equiv (P.reflectionPerm i)
      (fun j ↦ (P.coroot' (P.reflectionPerm i j) x) * (P.coroot' (P.reflectionPerm i j) y))
      (fun j ↦ P.coroot' j x * P.coroot' j y) (congrFun rfl)

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