Def RingQuot.natCast

Modification history

2025-12-17 09:29
Mathlib/Algebra/RingQuot.lean
feat: avoid `private irreducible_def` using module system (#32861) …
Added RingQuot.natCastView on Github →