Theorem Setoid.mk_eq_bot

Modification history

2025-11-24 14:10

Mathlib/Data/Setoid/Basic.lean

feat(Algebra): characterise when a quotient is nontrivial (#31198) …

Added Setoid.mk_eq_bot View on Github →