coroot_eq_coreflection_of_root_eq

English

If hk is the relation root k = reflection i (root j), then the corresponding coroots satisfy coroot k = coreflection i (coroot j).

Русский

Если отношение hk задаёт корень k через корень j после отражения i, то соответствующие короты удовлетворяют coroot k = coreflection i (coroot j).

LaTeX

$$$ P.root(k) = P.reflection(i)(P.root(j)) \Rightarrow P.coroot(k) = P.coreflection(i)(P.coroot(j)) $$$

Lean4

theorem coroot_eq_coreflection_of_root_eq {i j k : ι} (hk : P.root k = P.reflection i (P.root j)) :
    P.coroot k = P.coreflection i (P.coroot j) :=
  by
  rw [← P.root_reflectionPerm, EmbeddingLike.apply_eq_iff_eq] at hk
  rw [← P.coroot_reflectionPerm, hk]

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