Theorems · Theorem · commutative algebra
Nat.cast_eq_zero
∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] {n : ℕ}, ↑n = 0 ↔ n = 0- Defined in
- Mathlib.Algebra.CharZero.Defs
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 7 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_zeroproof · cited by 1,870
- CharZerostatement and proof · cited by 932
- AddMonoidWithOnestatement and proof · cited by 313
- Nat.cast_injproof · cited by 70
Cited by18
Results whose statement or proof uses this declaration.
- Nat.cast_ne_zeroproof · cited by 113
- Int.cast_eq_zeroproof · cited by 6
- LieAlgebra.Basis.iSupIndep_rootSpaceproof · cited by 3
- IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_ne_zero_of_eq_natproof · cited by 2
- Real.dimH_ball_piproof · cited by 2
- X_pow_sub_C_irreducible_of_primeproof · cited by 2
- spectralValue_X_powproof · cited by 2
- PowerSeries.exp_mul_exp_eq_exp_addproof · cited by 2
- Submodule.disjoint_ker_of_finrank_leproof · cited by 2
- FractionalIdeal.count_coeproof · cited by 1
- Real.log_nat_eq_sum_factorizationproof · cited by 1