Theorems · Definition · ring theory
Subsemigroup.corner
{R : Type u_1} → R → [inst : Semigroup R] → Subsemigroup RThe corner associated to an element e in a semigroup
is the subsemigroup of all elements of the form e * r * e.
- Defined in
- Mathlib.RingTheory.Idempotents
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses propext
- Assumes
- Semigroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.rangeproof · cited by 4,705
- Subsemigroupstatement · cited by 323
- Semigroupstatement and proof · cited by 202
Cited by7
Results whose statement or proof uses this declaration.
- Subsemigroup.mem_corner_iffstatement and proof · cited by 1
- Subsemigroup.mem_corner_iff_mem_range_mul_leftstatement · cited by 1
- Subsemigroup.mem_corner_iff_mul_leftstatement · cited by 1
- NonUnitalSubsemiring.cornerproof · cited by 0
- Subsemigroup.mem_corner_iff_mem_range_mul_rightstatement · cited by 0
- Subsemigroup.mem_corner_iff_mul_rightstatement · cited by 0
- IsIdempotentElem.Cornerproof · cited by 0