Swapping two entries of an additive family

This file records the elementary identity expressing a transposition of an additive family as a reflection. It is shared by coordinate and type-A root-datum constructions.

theorem TauCeti.apply_swap_eq {ι : Type u_1} {M : Type u_2} [DecidableEq ι] [AddCommGroup M] (f : ι → M) (a b c : ι) : f ((Equiv.swap a b) c) = f c - ((if c = a then 1 else 0) - if c = b then 1 else 0) • (f a - f b)

Transposing a family along Equiv.swap a b subtracts the corresponding multiple of f a - f b. This is the elementary identity behind coordinate reflection formulas.