Commit 2022-12-06 01:47 bc09bc5a

View on Github →

feat: port Algebra.Group.TypeTags (#832) Mathlib 6eb334bd8f3433d5b08ba156b8ec3e6af47e1904

Estimated changes

added def Additive.ofMul
added theorem Additive.ofMul_symm_eq
added def Additive.toMul
added theorem Additive.toMul_symm_eq
added def Additive
added def Multiplicative
added theorem ofAdd_add
added theorem ofAdd_eq_one
added theorem ofAdd_neg
added theorem ofAdd_sub
added theorem ofAdd_toAdd
added theorem ofAdd_zero
added theorem ofMul_div
added theorem ofMul_eq_zero
added theorem ofMul_inv
added theorem ofMul_mul
added theorem ofMul_one
added theorem ofMul_toMul
added theorem toAdd_div
added theorem toAdd_inv
added theorem toAdd_mul
added theorem toAdd_ofAdd
added theorem toAdd_one
added theorem toMul_add
added theorem toMul_neg
added theorem toMul_ofMul
added theorem toMul_sub
added theorem toMul_zero