Theorems · Theorem · field theory
sub_div
∀ {K : Type u_1} [inst : DivisionRing K] (a b c : K), (a - b) / c = a / c - b / c- Defined in
- Mathlib.Algebra.Field.Basic
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 46 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DivisionRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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
- div_sub_div_sameproof · cited by 11
Cited by37
Results whose statement or proof uses this declaration.
- Real.Icc_eq_closedBallproof · cited by 6
- integral_cpowproof · cited by 5
- Complex.tan_addproof · cited by 5
- HurwitzZeta.completedHurwitzZetaEven_eqproof · cited by 4
- HurwitzZeta.completedHurwitzZetaEven_one_subproof · cited by 3
- Real.abs_sin_halfproof · cited by 3
- Asymptotics.isEquivalent_iff_tendsto_oneproof · cited by 3
- Pell.exists_of_not_isSquareproof · cited by 3
- CircleDeg1Lift.transnumAuxSeq_dist_ltproof · cited by 2
- HurwitzZeta.completedHurwitzZetaEven_residue_oneproof · cited by 2
- Affine.Simplex.points_vsub_eulerPointproof · cited by 2
- HurwitzZeta.completedHurwitzZetaEven₀_one_subproof · cited by 2