English
If i and j are orthogonal, then the reflections P.reflection i and P.reflection j commute.
Русский
Если i и j ортогональны, то отображения отражений P.reflection i и P.reflection j commute.
LaTeX
$$$$ \\text{If } \\mathrm{IsOrthogonal}(P,i,j), \\; \\mathrm{reflection}_i \\circ \\mathrm{reflection}_j = \\mathrm{reflection}_j \\circ \\mathrm{reflection}_i. $$$$
Lean4
theorem isOrthogonal_comm (h : IsOrthogonal P i j) : Commute (P.reflection i) (P.reflection j) :=
by
rw [commute_iff_eq]
ext v
replace h : P.pairing i j = 0 ∧ P.pairing j i = 0 := by simpa [IsOrthogonal] using h
erw [Module.End.mul_apply, Module.End.mul_apply]
simp only [LinearEquiv.coe_coe, reflection_apply, LinearMap.flip_apply, map_sub, map_smul, root_coroot_eq_pairing, h,
zero_smul, sub_zero]
abel
