Commit 2022-05-14 05:39 38244939

View on Github →

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.

Estimated changes

Modified src/group_theory/free_abelian_group.lean

added theorem free_abelian_group.lift_neg'

deleted theorem free_abelian_group.map_add

deleted theorem free_abelian_group.map_neg

deleted theorem free_abelian_group.map_sub

deleted theorem free_abelian_group.map_zero

modified theorem free_abelian_group.mul_def

modified theorem free_abelian_group.of_mul_of