Def StarMulEquiv.Simps.symm_apply

Modification history

2025-08-06 01:34
Mathlib/Algebra/Star/MonoidHom.lean
feat: define morphism type `StarMonoidHom` (#27763) …
Added StarMulEquiv.Simps.symm_applyView on Github →