Commit 2024-06-08 16:29 fa72f05e

View on Github →

chore(Order/Basic): cleanup redundant type arguments (#13604)

Estimated changes

Modified Mathlib/Order/Basic.lean

modified def AsLinearOrder

modified theorem LinearOrder.ext

modified theorem LinearOrder.toPartialOrder_injective

modified def Order.Preimage

modified theorem PartialOrder.ext

modified theorem PartialOrder.toPreorder_injective

modified theorem Pi.compl_apply

modified theorem Pi.compl_def

modified theorem Pi.le_def

modified theorem Pi.lt_def

modified theorem Pi.sdiff_apply

modified theorem Pi.sdiff_def

modified theorem Preorder.ext

modified theorem Preorder.toLE_injective

modified theorem eq_iff_not_lt_of_le