Theorems · Theorem · ring theory
Subsemigroup.mem_corner_iff_mul_left
∀ {R : Type u_1} {e : R} [inst : Semigroup R],
IsIdempotentElem e → IsMulCentral e → ∀ {r : R}, r ∈ Subsemigroup.corner e ↔ e * r = r- Defined in
- Mathlib.RingTheory.Idempotents
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses propext
- Assumes
- Semigroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Subsemigroupstatement · cited by 323
- IsIdempotentElemstatement and proof · cited by 217
- Semigroupstatement and proof · cited by 202
- IsMulCentral.commproof · cited by 26
- IsMulCentralstatement and proof · cited by 13
- Subsemigroup.cornerstatement · cited by 5
- Subsemigroup.mem_corner_iffproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- Subsemigroup.mem_corner_iff_mul_rightproof · cited by 0