Theorem Quotient.lift_comp_mk

Modification history

2024-10-09 14:28

Mathlib/Data/Quot.lean

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

Modified Quotient.lift_comp_mk View on Github →

2022-11-10 23:34

Mathlib/Data/Quot.lean

feat: port Data.Quot (#559) …

Added Quotient.lift_comp_mk View on Github →