English
Same as the previous, under corresponding hypotheses, i.e., if P.root j = t · P.root i, then t · P.coroot j = P.coroot i.
Русский
То же самое, что и ранее: если P.root j = t · P.root i, тогда t · P.coroot j = P.coroot i.
LaTeX
$$$ P.root(j) = t \cdot P.root(i) \Rightarrow t \cdot P.coroot(j) = P.coroot(i) $$$
Lean4
theorem smul_coroot_eq_of_root_eq_smul [Finite ι] [NoZeroSMulDivisors ℤ N] (i j : ι) (t : R)
(h : P.root j = t • P.root i) : t • P.coroot j = P.coroot i :=
by
have hij : t * P.pairing i j = 2 := by simpa using ((P.coroot' j).congr_arg h).symm
refine
Module.eq_of_mapsTo_reflection_of_mem (f := P.root' i) (g := P.root' i) (finite_range P.coroot) (by simp [hij])
(by simp) (by simp [hij]) (by simp) ?_ (P.mapsTo_coreflection_coroot i) (mem_range_self i)
convert P.mapsTo_coreflection_coroot j
ext x
replace h : P.root' j = t • P.root' i := by ext; simp [h, root']
simp [Module.preReflection_apply, coreflection_apply, h, smul_comm _ t, mul_smul]
