Theorems · Theorem · field theory
Nat.cast_div
∀ {K : Type u_1} [inst : DivisionSemiring K] {m n : ℕ}, n ∣ m → ↑n ≠ 0 → ↑(m / n) = ↑m / ↑n- Defined in
- Mathlib.Data.Nat.Cast.Field
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext
- Assumes
- DivisionSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- mul_commproof · cited by 2,262
- Nat.cast_zeroproof · cited by 1,870
- Nat.cast_mulproof · cited by 309
- DivisionSemiringstatement and proof · cited by 216
- mul_div_cancel_right₀proof · cited by 70
Cited by8
Results whose statement or proof uses this declaration.
- Nat.cast_div_charZeroproof · cited by 6
- IsNilpotent.exp_add_of_commuteproof · cited by 3
- isEquivalent_chooseproof · cited by 2
- sum_range_powproof · cited by 2
- Algebra.discr_powerBasis_eq_prod''proof · cited by 1
- Nat.cast_div_div_div_cancel_rightproof · cited by 0
- DihedralGroup.commProb_reciprocalproof · cited by 0
- ArithmeticFunction.sum_moebius_mul_log_eqproof · cited by 0