Commit 2026-02-13 21:13 58a7fd71

View on Github →

feat(Data/Sym/Sym2): fromRel is injective & more (#34671)

Estimated changes

Modified Mathlib/Data/Sym/Sym2.lean

modified theorem Sym2.fromRel_bot

added theorem Sym2.fromRel_bot_iff

added theorem Sym2.fromRel_eq_fromRell_iff_eq

modified theorem Sym2.fromRel_top

added theorem Sym2.fromRel_top_iff