Theorems · Theorem · field theory
Rat.cast_div
∀ {α : Type u_3} [inst : DivisionRing α] [CharZero α] (p q : ℚ), ↑(p / q) = ↑p / ↑q- Defined in
- Mathlib.Data.Rat.Cast.CharZero
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DivisionRingCharZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DivisionRingstatement and proof · cited by 1,062
- CharZerostatement and proof · cited by 932
- map_div₀proof · cited by 98
- Rat.castHomproof · cited by 33
Cited by37
Results whose statement or proof uses this declaration.
- exists_rat_btwnproof · cited by 26
- isCusp_SL2Z_iffproof · cited by 3
- Rat.cast_divIntproof · cited by 3
- Real.exists_isLUBproof · cited by 3
- bernoulliFun_eval_oneproof · cited by 3
- Complex.isPrimitiveRoot_exp_ratproof · cited by 2
- LiouvilleWith.add_ratproof · cited by 2
- Rel.abs_edgeDensity_sub_edgeDensity_le_two_mul_sub_sqproof · cited by 1
- niven_angle_div_pi_eqproof · cited by 1
- irrational_iff_ne_rationalproof · cited by 1
- hasSum_zeta_fourproof · cited by 1
- ArchimedeanClass.FiniteResidueField.mk_ratCastproof · cited by 1