Mathlib v3 is deprecated. Go to Mathlib v4

Theorem multiplicative.to_add_symm_eq

Modification history

2020-10-17 20:50
src/algebra/group/type_tags.lean
chore(group/type_tags): Add missing simp lemmas (#4651)
Added multiplicative.to_add_symm_eqView on Github →