Theorem Quotient.liftOn₂_mk
Modification history
2025-08-04 09:17
Mathlib/Data/Quot.lean
chore(Quot): fix `Quotient.liftOn₂_mk` (#27303)
Modified Quotient.liftOn₂_mkView on Github →2024-10-09 14:28
Mathlib/Data/Quot.lean
chore(Data/Quot): `[s : Setoid α]` => `{s : Setoid α}` (#16256)
Modified Quotient.liftOn₂_mkView on Github →