Theorems · Theorem · order theory
Nat.cast_max
∀ {α : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (m n : ℕ), ↑(max m n) = max ↑m ↑n- Defined in
- Mathlib.Data.Nat.Cast.Order.Ring
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- LinearOrderstatement and proof · cited by 8,572
- IsStrictOrderedRingstatement and proof · cited by 2,490
- Nat.mono_castproof · cited by 76
- Monotone.map_maxproof · cited by 55
Cited by10
Results whose statement or proof uses this declaration.
- EisensteinSeries.norm_eq_max_natAbsproof · cited by 8
- EisensteinSeries.summable_one_div_norm_rpowproof · cited by 4
- Rat.mulHeight₁_eq_maxproof · cited by 2
- padicValRat_two_harmonicproof · cited by 2
- SzemerediRegularity.hundred_lt_pow_initialBound_mulproof · cited by 1
- Nat.cast_finsetSupproof · cited by 1
- EisensteinSeries.norm_symmproof · cited by 0
- EisensteinSeries.abs_le_left_of_normproof · cited by 0
- EisensteinSeries.abs_le_right_of_normproof · cited by 0
- Nat.cast_finsetSup'proof · cited by 0