Theorems · Theorem · commutative algebra
Nat.cast_add_one
∀ {R : Type u_1} [inst : AddMonoidWithOne R] (n : ℕ), ↑(n + 1) = ↑n + 1- Defined in
- Mathlib.Data.Nat.Cast.Defs
- Cited by
- 56 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
- Assumes
- AddMonoidWithOne
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.
- AddMonoidWithOnestatement and proof · cited by 313
- Nat.cast_succproof · cited by 99
Cited by56
Results whose statement or proof uses this declaration.
- Cardinal.natCast_lt_aleph0proof · cited by 47
- ONote.fundamentalSequence_has_propproof · cited by 5
- CircleDeg1Lift.translationNumber_le_of_le_add_intproof · cited by 4
- Polynomial.derivative_eq_zeroproof · cited by 4
- Real.log_zpowproof · cited by 4
- Cardinal.exists_ne_ne_of_three_leproof · cited by 4
- Ordinal.nat_lt_cardproof · cited by 4
- Finset.box_succ_eq_sdiffproof · cited by 4
- sum_mul_eq_sub_sub_integral_mulproof · cited by 4
- Real.strictMono_eulerMascheroniSeqproof · cited by 3
- Ordinal.lt_omega0_opowproof · cited by 3
- integrableOn_mul_sum_Iccproof · cited by 3