Commit 2025-11-07 14:41 117f377c

View on Github →

feat(Data/Sym/Sym2): fromRel is monotonic (#30542)

Estimated changes

Modified Mathlib/Data/Sym/Sym2.lean

added def Sym2.fromRelOrderEmbedding

added theorem Sym2.fromRel_mono_iff