Commit 2026-02-11 12:13 0528bce2

View on Github →

chore(Order/Defs/Unbundled): deprecate def Total in favor of class Std.Total (#34351)

Estimated changes

Modified Mathlib/ModelTheory/Order.lean

Modified Mathlib/ModelTheory/Semantics.lean

modified theorem FirstOrder.Language.Relations.realize_total

Modified Mathlib/Order/Defs/Unbundled.lean