Theorems · Theorem · commutative algebra
Convex.combo_self
∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {a b : R},
a + b = 1 → ∀ (x : M), a • x + b • x = x- Defined in
- Mathlib.Algebra.Module.Defs
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses no axioms
- Assumes
- SemiringAddCommMonoidModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- one_smulproof · cited by 1,374
- add_smulproof · cited by 204
Cited by29
Results whose statement or proof uses this declaration.
- convex_Iicproof · cited by 12
- convexOn_constproof · cited by 6
- invOf_two_smul_add_invOf_two_smulproof · cited by 6
- convex_Iioproof · cited by 6
- segment_subset_Iccproof · cited by 4
- ConvexOn.le_left_of_right_le'proof · cited by 3
- convex_iff_pairwise_posproof · cited by 3
- convexOn_iff_pairwise_posproof · cited by 3
- ConvexOn.lt_left_of_right_lt'proof · cited by 3
- ConvexOn.convex_leproof · cited by 3
- ConvexOn.convex_ltproof · cited by 3
- openSegment_subset_Iooproof · cited by 2