Theorems · Theorem · order theory
WithBot.coe_lt_coe
∀ {α : Type u_1} {a b : α} [inst : LT α], ↑a < ↑b ↔ a < b- Defined in
- Mathlib.Order.WithBot
- Cited by
- 55 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext, Quot.sound
- Assumes
- LT
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- WithBotstatement · cited by 1,498
- WithBot.somestatement · cited by 541
Cited by55
Results whose statement or proof uses this declaration.
- Polynomial.eq_C_of_degree_le_zeroproof · cited by 20
- EReal.coe_lt_topproof · cited by 17
- Polynomial.modByMonic_eq_zero_iff_dvdproof · cited by 15
- Polynomial.modByMonic_X_sub_C_eq_C_evalproof · cited by 7
- Polynomial.associated_content_mulproof · cited by 6
- WithBot.preimage_coe_Iioproof · cited by 6
- WithBot.coe_strictMonoproof · cited by 6
- Polynomial.coeff_mul_degree_add_degreeproof · cited by 5
- WithBot.preimage_coe_Ioiproof · cited by 4
- Lagrange.degree_interpolate_ltproof · cited by 4
- Polynomial.degree_sum_fin_ltproof · cited by 4
- Polynomial.degree_derivative_ltproof · cited by 4