Theorems · Theorem · field theory
Nat.cast_div_charZero
∀ {K : Type u_1} [inst : DivisionSemiring K] {m n : ℕ} [CharZero K], n ∣ m → ↑(m / n) = ↑m / ↑n- Defined in
- Mathlib.Data.Nat.Cast.Field
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DivisionSemiringCharZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- eq_or_neproof · cited by 1,117
- CharZerostatement and proof · cited by 932
- div_zeroproof · cited by 251
- DivisionSemiringstatement and proof · cited by 216
- Nat.cast_divproof · cited by 8
Cited by6
Results whose statement or proof uses this declaration.
- PowerSeries.exp_mul_exp_eq_exp_addproof · cited by 2
- DihedralGroup.commProb_oddproof · cited by 1
- bernoulliPowerSeries_mul_exp_sub_oneproof · cited by 1
- bernoulli'PowerSeries_mul_exp_sub_oneproof · cited by 1
- Nat.totient_eq_mul_prod_factorsproof · cited by 0
- numDerangements_tendsto_inv_eproof · cited by 0