Theorems · Theorem · field theory
Rat.cast_add
∀ {α : Type u_3} [inst : DivisionRing α] [CharZero α] (p q : ℚ), ↑(p + q) = ↑p + ↑q- Defined in
- Mathlib.Data.Rat.Cast.CharZero
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 70 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.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LT.lt.ne'proof · cited by 1,417
- DivisionRingstatement and proof · cited by 1,062
- CharZerostatement and proof · cited by 932
- Nat.cast_ne_zeroproof · cited by 113
- Rat.posproof · cited by 17
- Rat.cast_add_of_ne_zeroproof · cited by 2
Cited by20
Results whose statement or proof uses this declaration.
- Rat.castHomproof · cited by 33
- Rat.round_castproof · cited by 3
- AntitoneOn.integral_le_sumproof · cited by 3
- Real.strictMono_eulerMascheroniSeqproof · cited by 3
- AntitoneOn.sum_le_integralproof · cited by 2
- Real.strictAnti_eulerMascheroniSeq'proof · cited by 2
- ZetaAsymptotics.termSum_oneproof · cited by 2
- sum_Ico_le_integral_of_leproof · cited by 2
- Real.deriv_Gamma_natproof · cited by 2
- LinearOrderedField.cutMap_addproof · cited by 1
- GaussianInt.toComplex_re_divproof · cited by 1
- sum_mul_Ico_le_integral_of_monotone_antitoneproof · cited by 1