Theorems · Theorem · number theory
one_lt_two
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1]
[AddLeftStrictMono α], 1 < 2- Defined in
- Mathlib.Algebra.Order.Monoid.NatCast
- Cited by
- 67 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement and proof · cited by 6,410
- AddMonoidWithOnestatement and proof · cited by 313
- ZeroLEOneClassstatement and proof · cited by 304
- AddLeftStrictMonostatement and proof · cited by 203
- lt_add_oneproof · cited by 105
- one_add_one_eq_twoproof · cited by 65
Cited by67
Results whose statement or proof uses this declaration.
- Squarefree.isRadicalproof · cited by 7
- IsSelfAdjoint.spectralRadius_eq_nnnormproof · cited by 7
- hasFDerivAt_ringInverseproof · cited by 5
- IsPrimitiveRoot.eq_neg_one_of_two_rightproof · cited by 5
- Nat.totient_evenproof · cited by 4
- Complex.tsum_exp_neg_quadraticproof · cited by 3
- midpoint_mem_openSegmentproof · cited by 3
- Polynomial.cyclotomic_coeff_zeroproof · cited by 3
- Ordinal.isSuccLimit_of_isPrincipal_mulproof · cited by 3
- IsPrimitiveRoot.norm_sub_one_twoproof · cited by 3
- FormalMultilinearSeries.comp_summable_nnrealproof · cited by 2