Theorem Sym2.fromRel_eq_fromRell_iff_eq

Modification history

2026-02-13 21:13
Mathlib/Data/Sym/Sym2.lean
feat(Data/Sym/Sym2): `fromRel` is injective & more (#34671)
Added Sym2.fromRel_eq_fromRell_iff_eqView on Github →