Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-17 20:50 03674679

View on Github →

chore(group/type_tags): Add missing simp lemmas (#4651)

Estimated changes

Modified src/algebra/group/type_tags.lean

modified def additive.of_mul

added theorem additive.of_mul_symm_eq

modified def additive.to_mul

added theorem additive.to_mul_symm_eq

modified def multiplicative.of_add

added theorem multiplicative.of_add_symm_eq

modified def multiplicative.to_add

added theorem multiplicative.to_add_symm_eq