Theorems · Theorem · commutative algebra
Nat.cast_sub
∀ {R : Type u} [inst : AddGroupWithOne R] {m n : ℕ}, m ≤ n → ↑(n - m) = ↑n - ↑m- Defined in
- Mathlib.Data.Int.Cast.Basic
- Cited by
- 54 results in Mathlib
- Foundations
- Depth 17 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.
- Nat.cast_addproof · cited by 586
- AddGroupWithOnestatement and proof · cited by 111
- eq_sub_of_add_eqproof · cited by 21
Cited by54
Results whose statement or proof uses this declaration.
- Int.cast_subNatNatproof · cited by 6
- LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeffproof · cited by 6
- PadicInt.zmod_cast_comp_toZModPowproof · cited by 4
- AntitoneOn.sum_le_integral_Icoproof · cited by 3
- descPochhammer_eval_eq_descFactorialproof · cited by 3
- ZMod.cast_addproof · cited by 3
- AntitoneOn.integral_le_sum_Icoproof · cited by 3
- ZMod.cast_mulproof · cited by 3
- norm_root_le_spectralValueproof · cited by 3
- spectralValue_X_powproof · cited by 2
- Chebyshev.abs_psi_sub_theta_le_sqrt_mul_logproof · cited by 2
- dvd_pow_pow_sub_self_of_dvdproof · cited by 2