Theorem Sym2.fromRel_top

Modification history

2026-02-13 21:13
Mathlib/Data/Sym/Sym2.lean
feat(Data/Sym/Sym2): `fromRel` is injective & more (#34671)
Modified Sym2.fromRel_topView on Github →
2024-10-14 12:17
Mathlib/Data/Sym/Sym2.lean
chore: unused arguments (#17348)
Modified Sym2.fromRel_topView on Github →
2023-05-07 05:02
Mathlib/Data/Sym/Sym2.lean
chore: bye-bye, solo `by`s! (#3825) …
Modified Sym2.fromRel_topView on Github →
2023-01-27 10:07
Mathlib/Data/Sym/Sym2.lean
feat: Port `Data.Sym.Sym2` (#1805)
Added Sym2.fromRel_topView on Github →