Commit 2024-12-07 13:24 6b4fc18b

View on Github →

refactor(Order/Basic): Make LinearOrder α = LinearOrder αᵒᵈᵒᵈ defeq (#19776)

Estimated changes

Modified Mathlib/Order/Basic.lean

added theorem OrderDual.Ord.dual_dual