Theorems · Theorem · field theory
add_self_div_two
∀ {K : Type u_1} [inst : DivisionSemiring K] [NeZero 2] (a : K), (a + a) / 2 = a- Defined in
- Mathlib.Algebra.Field.Basic
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext
- Assumes
- DivisionSemiringNeZero
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.
- two_ne_zeroproof · cited by 251
- DivisionSemiringstatement and proof · cited by 216
- mul_div_cancel_right₀proof · cited by 70
- mul_twoproof · cited by 43
Cited by18
Results whose statement or proof uses this declaration.
- add_halvesproof · cited by 78
- Complex.cos_zeroproof · cited by 14
- Real.sinh_arsinhproof · cited by 8
- Real.Icc_eq_closedBallproof · cited by 6
- HurwitzZeta.sinKernel_defproof · cited by 5
- Complex.cosh_zeroproof · cited by 3
- Affine.Triangle.dist_orthocenter_reflection_circumcenterproof · cited by 3
- Complex.cos_sub_cosproof · cited by 3
- Complex.sin_sub_sinproof · cited by 3
- CurveIntegrable.intervalIntegrable_curveIntegralFun_trans_rightproof · cited by 2
- Complex.inv_Gammaℝ_two_subproof · cited by 2
- Complex.sqrt_neg_of_nonnegproof · cited by 2