Commit 2026-01-08 06:50 98379c78

View on Github →

chore(Order/Defs/Unbundled): deprecate IsIrrefl in favor of core's Std.Irrefl (#33717)

Estimated changes

modified theorem DFinsupp.lex_iff_of_unique
modified theorem Finsupp.lex_iff_of_unique
modified theorem List.lex_cons_iff
modified theorem List.shortlex_cons_iff
modified theorem List.Pairwise.eq_of_mem_iff
modified theorem Acc.cutExpand
modified theorem Relation.acc_of_singleton
modified theorem Relation.cutExpand_closed
modified theorem Relation.cutExpand_iff
modified theorem Relation.not_cutExpand_zero
modified theorem IncompRel.refl
modified theorem IncompRel.rfl
modified theorem irrefl
modified theorem irrefl_of
modified theorem ne_of_irrefl'
modified theorem ne_of_irrefl
modified theorem not_rel_of_subsingleton
modified theorem PrincipalSeg.ext
modified theorem Pi.lex_iff_of_unique
deleted theorem IsIrrefl.swap
added theorem Std.Irrefl.swap
modified theorem Subsingleton.isWellOrder
modified theorem eq_empty_relation
modified theorem ne_of_ssubset
modified theorem ne_of_ssuperset
modified theorem ssubset_irrefl
modified theorem ssubset_irrfl