Theorems · Theorem · commutative algebra
SemiconjBy.add_right
∀ {R : Type u} [inst : Distrib R] {a x y x' y' : R},
SemiconjBy a x y → SemiconjBy a x' y' → SemiconjBy a (x + x') (y + y')- Defined in
- Mathlib.Algebra.Ring.Semiconj
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses propext
- Assumes
- Distrib
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.
- SemiconjBystatement and proof · cited by 99
- Distribstatement and proof · cited by 31
- right_distribproof · cited by 26
- left_distribproof · cited by 19
- SemiconjBy.eqproof · cited by 18
Cited by2
Results whose statement or proof uses this declaration.
- Commute.add_rightproof · cited by 5
- SemiconjBy.sub_rightproof · cited by 1