Mathlib Map

Theorems · Theorem · commutative algebra

SemiconjBy.add_left

∀ {R : Type u} [inst : Distrib R] {a b x y : R}, SemiconjBy a x y → SemiconjBy b x y → SemiconjBy (a + b) x y
Defined in
Mathlib.Algebra.Ring.Semiconj
Cited by
2 results in Mathlib
Foundations
Depth 6 from the axioms · uses propext
Assumes
Distrib
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Commute.add_left · cited by 9Commute.add_leftSemiconjBy.sub_left · cited by 1SemiconjBy.sub_leftSemiconjBy · cited by 99SemiconjByDistrib · cited by 31Distribright_distrib · cited by 26right_distribleft_distrib · cited by 19left_distribSemiconjBy.eq · cited by 18SemiconjBy.eqSemiconjBy.add_leftCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.