rootLength_pos — Mathlib

English

The rootLength after applying a reflection permutation equals the original rootLength: B.rootLength (P.reflectionPerm i i) = B.rootLength i.

Русский

Длина корня после применения перестановки отражения равна исходной длине: B.rootLength (P.reflectionPerm i i) = B.rootLength i.

LaTeX

$$$ B.rootLength( P.reflectionPerm\\ i\\ i ) = B.rootLength\\ i $$$

Lean4

theorem rootLength_pos (i : ι) : 0 < B.rootLength i := by simpa using B.zero_lt_posForm_apply_root i

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