Theorem Quotient.map'_mk

Modification history

2024-10-09 14:28

Mathlib/Data/Quot.lean

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

Modified Quotient.map'_mk View on Github →

2022-11-10 23:34

Mathlib/Data/Quot.lean

feat: port Data.Quot (#559) …

Added Quotient.map'_mk View on Github →