mathlib

16ecb3d1 - chore(algebra/group/type_tags): missing simp lemmas (#13553)

chore(algebra/group/type_tags): missing simp lemmas (#13553) To have `simps` generate these in an appropriate form, this inserts explicits coercions between the type synonyms.