Def NonUnitalStarRingHom.ofClass

Modification history

2026-09-07 13:06
Mathlib/Algebra/Star/StarRingHom.lean
chore: standardise names for coercions from morphism classes to morphisms (#43367) …
Added NonUnitalStarRingHom.ofClassView on Github →