Theorems · Theorem · ring theory
StarAddMonoid.star_add
∀ {R : Type u} {inst : AddMonoid R} [self : StarAddMonoid R] (r s : R), star (r + s) = star r + star sstar commutes with addition
- Defined in
- Mathlib.Algebra.Star.Basic
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- StarAddMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddMonoidstatement and proof · cited by 2,864
- Star.starstatement · cited by 1,082
- StarAddMonoidstatement and proof · cited by 296
Cited by30
Results whose statement or proof uses this declaration.
- starAddEquivproof · cited by 25
- IsSelfAdjoint.addproof · cited by 8
- star_le_star_iffproof · cited by 6
- Matrix.PosSemidef.submatrixproof · cited by 3
- IsSelfAdjoint.of_geproof · cited by 2
- IsSelfAdjoint.star_add_selfproof · cited by 1
- CStarModule.inner_add_leftproof · cited by 1
- Matrix.PosDef.submatrixproof · cited by 1
- AddConGen.Rel.starproof · cited by 1
- star_mul_self_add_self_mul_starproof · cited by 1
- star_mul_self_eq_realPart_sq_add_imaginaryPart_sqproof · cited by 1
- star_mul_self_sub_self_mul_starproof · cited by 1