Theorems · Theorem · field theory
Nat.cast_div_div_div_cancel_right
∀ {K : Type u_1} [inst : DivisionSemiring K] {d m n : ℕ} [CharZero K], d ∣ n → d ∣ m → ↑(m / d) / ↑(n / d) = ↑m / ↑n- Defined in
- Mathlib.Data.Nat.Cast.Field
- Cited by
- 0 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.
Cites8
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
- zero_divproof · cited by 222
- DivisionSemiringstatement and proof · cited by 216
- Nat.cast_divproof · cited by 8
- div_div_div_cancel_right₀proof · cited by 6
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.