Theorems · Theorem · commutative algebra
Nat.cast_pred
∀ {R : Type u} [inst : AddGroupWithOne R] {n : ℕ}, 0 < n → ↑(n - 1) = ↑n - 1- Defined in
- Mathlib.Data.Int.Cast.Basic
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
- Assumes
- AddGroupWithOne
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- add_sub_cancel_rightproof · cited by 187
- AddGroupWithOnestatement and proof · cited by 111
- Nat.cast_succproof · cited by 99
Cited by8
Results whose statement or proof uses this declaration.
- SimpleGraph.antitoneOn_extremalNumber_div_choose_twoproof · cited by 3
- schnirelmannDensity_le_of_notMemproof · cited by 2
- LucasLehmer.residue_eq_zero_iff_sMod_eq_zeroproof · cited by 2
- MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProdproof · cited by 2
- LucasLehmer.ω_pow_formulaproof · cited by 1
- Projectivization.card_of_finrankproof · cited by 1
- Nat.totient_eq_mul_prod_factorsproof · cited by 0
- ModularForm.prod_fintype_slashproof · cited by 0