English
For indices i, j, we have P.reflectionPerm i = P.reflectionPerm j if and only if the reflections agree on every vector x in the span of the roots, i.e., P.reflection i x = P.reflection j x for all x ∈ span_R(range P.root).
Русский
Для i, j верно: P.reflectionPerm i = P.reflectionPerm j если и только если отражения совпадают на каждом векторе x в линейном пространства span_R( range P.root ), то есть P.reflection i x = P.reflection j x для всех x ∈ span_R(range P.root).
LaTeX
$$$$ P.reflectionPerm i = P.reflectionPerm j \\iff \\forall x \\in \\operatorname{span}_R(\\operatorname{range}(P.root)),\\; P.reflection i\,x = P.reflection j\,x. $$$$
Lean4
theorem reflectionPerm_eq_reflectionPerm_iff_of_span :
P.reflectionPerm i = P.reflectionPerm j ↔ ∀ x ∈ span R (range P.root), P.reflection i x = P.reflection j x :=
by
refine ⟨fun h x hx ↦ ?_, fun h ↦ ?_⟩
·
induction hx using Submodule.span_induction with
| mem x hx =>
obtain ⟨k, rfl⟩ := hx
simp only [← root_reflectionPerm, h]
| zero => simp
| add x y _ _ hx hy => simp [hx, hy]
| smul t x _ hx => simp [hx]
· ext k
apply P.root.injective
simp [h (P.root k) (Submodule.subset_span <| mem_range_self k)]
