Theorem Quotient.eq_mk_iff_out

Modification history

2024-10-09 14:28

Mathlib/Data/Quot.lean

chore(Data/Quot): `[s : Setoid α]` => `{s : Setoid α}` (#16256)

Modified Quotient.eq_mk_iff_out View on Github →

2022-11-10 23:34

Mathlib/Data/Quot.lean

feat: port Data.Quot (#559) …

Added Quotient.eq_mk_iff_out View on Github →