Commit 2026-01-05 15:18 e01781fd

View on Github →

chore(Order/Defs/Unbundled): deprecate IsAsymm in favor of core's Std.Asymm (#33503)

Estimated changes

Modified Mathlib/Data/Finset/Defs.lean

Modified Mathlib/Data/List/Lex.lean

Modified Mathlib/Data/List/Shortlex.lean

Modified Mathlib/Data/Prod/Basic.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Data/Sigma/Lex.lean

Modified Mathlib/NumberTheory/Divisors.lean

Modified Mathlib/Order/Defs/Unbundled.lean

modified theorem asymm

modified theorem asymm_of

Modified Mathlib/Order/RelClasses.lean

deleted theorem IsAsymm.swap

added theorem Std.Asymm.swap

modified theorem isStrictWeakOrder_of_isOrderConnected

modified theorem ssubset_asymm

Modified Mathlib/Order/RelIso/Basic.lean

modified def RelEmbedding.ofMonotone

modified theorem RelEmbedding.ofMonotone_coe

Modified Mathlib/Order/RelIso/Set.lean

Modified Mathlib/Order/WellFounded.lean