Commit 2026-02-06 22:29 cb53e58e

View on Github →

chore: rename CompRel to Relation.SymmGen (#34428) See this Zulip thread. This PR renames CompRel to Relation.SymmGen for consistency with core and Mathlib.Logic.Relation. Import changes are avoided by moving declarations to Mathlib.Logic.Relation and Mathlib.Order.Antisymmetrization, which seems natural and is what #find_home suggests.

Estimated changes

added theorem Relation.SymmGen.of_ge
added theorem Relation.SymmGen.of_le
added theorem Relation.SymmGen.refl
added theorem Relation.SymmGen.rfl
added theorem Relation.SymmGen.swap
added theorem Relation.SymmGen.symm
added def Relation.SymmGen
added theorem Relation.symmGen_comm
added theorem Relation.symmGen_swap
added theorem AntisymmRel.symmGen
added theorem Relation.SymmGen.of_gt
added theorem Relation.SymmGen.of_lt
modified theorem CompRel.of_ge
modified theorem CompRel.of_gt
modified theorem CompRel.of_le
modified theorem CompRel.of_lt
modified theorem CompRel.rfl
modified theorem not_compRel_iff
modified theorem not_incompRel_iff
added theorem not_symmGen_iff