Theorem StarRingEquiv.symm_mk

Modification history

2026-05-12 14:07
Mathlib/Algebra/Star/StarRingHom.lean
chore: syntactically generalise `symm_mk` (#37748)
Modified StarRingEquiv.symm_mkView on Github →
2024-06-26 22:10
Mathlib/Algebra/Star/StarRingHom.lean
feat(Algebra/Star/StarRingHom): Add non-unital star ring homomorphisms (#12924) …
Added StarRingEquiv.symm_mkView on Github →