Theorem TwoSidedIdeal.coe_mk

Modification history

2025-04-18 00:22
Mathlib/RingTheory/TwoSidedIdeal/Basic.lean
feat: generalize `TwoSidedIdeal.matricesOver` to `RingCon` (#23641) …
Added TwoSidedIdeal.coe_mkView on Github →