English
If R is a nonunital ring and e is an idempotent, then the corner idem.Corner has a natural ring structure, i.e. idem.Corner is a (unital) ring with unit given by e.
Русский
Если R — кольцо без единицы и e — идемпотент, то уголок idem.Corner обладает естественной структурой кольца, то есть это кольцо с единицей, равной e.
LaTeX
$$$\\text{If } R \\text{ is a nonunital ring and } e^2 = e, \\text{ then } \\text{idem.Corner} \\text{ carries a ring structure with unit } e.$$$
Lean4
instance [NonUnitalRing R] (idem : IsIdempotentElem e) : Ring idem.Corner
where
__ : NonUnitalRing (NonUnitalRing.corner e) := inferInstance
__ : Semiring idem.Corner := inferInstance
