Commit 2026-02-16 11:54 41228da3

View on Github →

chore(Order/Defs/Unbundled): deprecate def Irreflexive in favor of class Std.Irrefl (#35191)

Estimated changes

Modified Archive/Wiedijk100Theorems/Konigsberg.lean

Modified Mathlib/Combinatorics/Digraph/Orientation.lean

Modified Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

Modified Mathlib/Combinatorics/SimpleGraph/Hasse.lean

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

Modified Mathlib/Combinatorics/SimpleGraph/Prod.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

Modified Mathlib/Combinatorics/SimpleGraph/Sum.lean

Modified Mathlib/Combinatorics/SimpleGraph/Trails.lean

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean

modified def SimpleGraph.TripartiteFromTriangles.graph

Modified Mathlib/Combinatorics/SimpleGraph/Walks/Basic.lean

Modified Mathlib/Data/List/MinMax.lean

modified theorem List.argAux_self

modified theorem List.not_of_mem_foldl_argAux

Modified Mathlib/Data/Sym/Sym2.lean

added theorem Sym2.fromRel_irrefl

deleted theorem Sym2.fromRel_irreflexive

modified theorem Sym2.mem_fromRel_irrefl_other_ne

Modified Mathlib/Logic/Relation.lean

added theorem irrefl_iff_subrelation_ne

deleted theorem irreflexive_iff_subrelation_ne

Modified Mathlib/ModelTheory/Graph.lean

Modified Mathlib/ModelTheory/Semantics.lean

modified theorem FirstOrder.Language.Relations.realize_irreflexive

Modified Mathlib/Order/Defs/Unbundled.lean

added theorem InvImage.irrefl

deleted theorem InvImage.irreflexive