Theorems · Theorem · commutative algebra
Nat.cast_add_one_ne_zero
∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] (n : ℕ), ↑n + 1 ≠ 0- Defined in
- Mathlib.Algebra.CharZero.Defs
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses propext
- Assumes
- AddMonoidWithOneCharZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.cast_oneproof · cited by 2,501
- Nat.cast_zeroproof · cited by 1,870
- CharZerostatement and proof · cited by 932
- AddMonoidWithOnestatement and proof · cited by 313
Cited by11
Results whose statement or proof uses this declaration.
- CircleDeg1Lift.translationNumber_translateproof · cited by 2
- IsSl2Triple.HasPrimitiveVectorWith.exists_natproof · cited by 2
- HurwitzZeta.hurwitzZetaEven_neg_two_mul_nat_add_oneproof · cited by 2
- sineTerm_ne_zeroproof · cited by 1
- taylor_mean_remainder_lagrangeproof · cited by 1
- MeasureTheory.Measure.MeasureDense.of_generateFrom_isSetAlgebra_finiteproof · cited by 1
- EulerSine.sin_pi_mul_eqproof · cited by 1
- Complex.not_continuousAt_Gamma_neg_natproof · cited by 1
- antideriv_bernoulliFunproof · cited by 1
- HurwitzZeta.cosZeta_neg_two_mul_nat_add_oneproof · cited by 0
- analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zeroproof · cited by 0