We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
decidableEqofDecidableLE'
1 parent f7442dd commit c91c157Copy full SHA for c91c157
Mathlib/Order/Defs/PartialOrder.lean
@@ -206,7 +206,7 @@ lemma lt_of_le_of_ne : a ≤ b → a ≠ b → a < b := fun h₁ h₂ =>
206
lt_of_le_not_ge h₁ <| mt (le_antisymm h₁) h₂
207
208
/-- Equality is decidable if `≤` is. -/
209
-@[to_dual decidableEqofDecidableLE' /-- Equality is decidable if `≤` is. -/]
+@[to_dual decidableEqOfDecidableLE' /-- Equality is decidable if `≤` is. -/]
210
def decidableEqOfDecidableLE [DecidableLE α] : DecidableEq α
211
| a, b =>
212
if hab : a ≤ b then
0 commit comments