mathlib

38244939 - refactor(group_theory/free_abelian_group): Make proofs more robust (#14089)

refactor(group_theory/free_abelian_group): Make proofs more robust (#14089) Reduce the API breakage by proving `distrib (free_abelian_group α)` and `has_distrib_neg (free_abelian_group α)` earlier. Protect lemmas to avoid shadowing the root ones. Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>