Theorem RingCon.coe_bot

Modification history

2025-11-24 14:10
Mathlib/RingTheory/Congruence/Basic.lean
feat(Algebra): characterise when a quotient is nontrivial (#31198) …
Modified RingCon.coe_botView on Github →
2024-05-14 16:33
Mathlib/RingTheory/Congruence.lean
feat: RingCon.coe_bot (#12860) …
Added RingCon.coe_botView on Github →