Mathlib v3 is deprecated. Go to Mathlib v4

Theorem sym2.is_diag.mem_range_diag

Modification history

2021-07-20 18:13

src/data/sym2.lean

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

Added sym2.is_diag.mem_range_diag View on Github →