Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-31 16:05 6ed6abbd

View on Github →

feat(data/quot): make trunc a quotient (#18320) This allows us to use quotient lemmas for trunc. mathlib4 PR: https://github.com/leanprover-community/mathlib4/pull/1924

Estimated changes

added def true_setoid
modified def {u}