Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-20 18:13 4676b31f

View on Github →

feat(data/sym2): add the universal property, and make sym2.is_diag ⟦(x, y)⟧ ↔ x = y true definitionally (#8358)

Estimated changes

modified def sym2.is_diag
added theorem sym2.is_diag_iff_eq
added def sym2.lift
added theorem sym2.lift_mk