English
Assume M is 2-regular in the sense IsSMulRegular M 2. For any i, j in ι, the equality of reflection permutations P.reflectionPerm i = P.reflectionPerm j is equivalent to the equality of reflections P.reflection i = P.reflection j.
Русский
Пусть M удовлетворяет условию IsSMulRegular 2. Тогда для любых i, j верно, что P.reflectionPerm i = P.reflectionPerm j эквивалентно P.reflection i = P.reflection j.
LaTeX
$$$$ P.reflectionPerm i = P.reflectionPerm j \\iff P.reflection i = P.reflection j. $$$$
Lean4
theorem reflectionPerm_eq_reflectionPerm_iff_of_isSMulRegular (h2 : IsSMulRegular M 2) :
P.reflectionPerm i = P.reflectionPerm j ↔ P.reflection i = P.reflection j :=
by
refine ⟨fun h ↦ ?_, fun h ↦ Equiv.ext fun k ↦ P.root.injective <| by simp [h]⟩
suffices ⇑(P.reflection i) = ⇑(P.reflection j) from DFunLike.coe_injective this
replace h2 : IsSMulRegular (M → M) 2 := IsSMulRegular.pi fun _ ↦ h2
exact h2 <| P.two_nsmul_reflection_eq_of_perm_eq i j h
