Theorem StarMulEquiv.toMulEquiv_symm

Modification history

2025-08-28 20:04
Mathlib/Algebra/Star/MonoidHom.lean
refactor: change `unitary.map` to take an explicit morphism as an argument, rather than a morphism class (#28122) …
Added StarMulEquiv.toMulEquiv_symmView on Github →