English
For all i, j, the root i equals minus root j if and only if i equals reflectionPerm(j, j).
Русский
Для любых i, j корень i равен минус корня j тогда и только тогда, когда i = reflectionPerm(j, j).
LaTeX
$$$ P.root(i) = -P.root(j) \iff i = P.reflectionPerm(j, j) $$$
Lean4
/-- The indexing set of a root pairing carries an involutive negation, corresponding to the negation
of a root / coroot. -/
@[simps]
def indexNeg : InvolutiveNeg ι where
neg i := P.reflectionPerm i i
neg_neg
i := by
apply P.root.injective
simp only [root_reflectionPerm, reflection_apply, LinearMap.flip_apply, root_coroot_eq_pairing, pairing_same,
map_sub, coroot_reflectionPerm, coreflection_apply_self, map_neg, neg_smul, sub_neg_eq_add, map_smul, smul_add]
module
