Theorems · Theorem · ring theory
Subsemigroup.mem_corner_iff_mem_range_mul_left
∀ {R : Type u_1} {e : R} [inst : Semigroup R],
IsIdempotentElem e → IsMulCentral e → ∀ {r : R}, r ∈ Subsemigroup.corner e ↔ r ∈ Set.range fun x => e * x- Defined in
- Mathlib.RingTheory.Idempotents
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses propext, Quot.sound
- Assumes
- Semigroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Set.rangestatement and proof · cited by 4,705
- Subsemigroupstatement · cited by 323
- IsIdempotentElemstatement and proof · cited by 217
- Semigroupstatement and proof · cited by 202
- Commute.eqproof · cited by 91
- IsIdempotentElem.eqproof · cited by 42
- IsMulCentral.commproof · cited by 26
- IsMulCentralstatement and proof · cited by 13
- Subsemigroup.cornerstatement · cited by 5
Cited by1
Results whose statement or proof uses this declaration.
- Subsemigroup.mem_corner_iff_mem_range_mul_rightproof · cited by 0