Mathlib Map

Theorems · Theorem · commutative algebra

IsAddRightRegular.add

∀ {R : Type u_1} [inst : AddSemigroup R] {a b : R},
  IsAddRightRegular a → IsAddRightRegular b → IsAddRightRegular (a + b)

In an additive semigroup, the sum of add-right-regular elements is add-right-regular.

Defined in
Mathlib.Algebra.Regular.Basic
Cited by
2 results in Mathlib
Foundations
Depth 7 from the axioms · uses propext, Quot.sound
Assumes
AddSemigroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsAddRegular.add · cited by 1IsAddRegular.addadd_isAddRightRegular_iff · cited by 0add_isAddRightRegular_iffAddSemigroup · cited by 136AddSemigroupIsAddRightRegular · cited by 55IsAddRightRegularcomp_add_right · cited by 4comp_add_rightIsAddRightRegular.addCITED BYCITES

Cites3

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.