English
If R is a nonunital semiring and e is an idempotent element, then the corner idem.Corner inherits a (nonunital) semiring structure, with the unit given by the element e.
Русский
Если R — полусемиринг без единицы, и e — идемпотент, то уголок idem.Corner наследует структуру полусемиринга, единица которого равна элементу e.
LaTeX
$$$\\text{If } R \\text{ is a nonunital semiring and } e^2 = e, \\text{ then } \\text{idem.Corner} \\\\text{ carries a semiring structure with } 1 = e.$$$
Lean4
instance [NonUnitalSemiring R] (idem : IsIdempotentElem e) : Semiring idem.Corner
where
__ : NonUnitalSemiring (NonUnitalSubsemiring.corner e) := inferInstance
one := ⟨e, e, by simp_rw [idem.eq]⟩
one_mul r := Subtype.ext ((Subsemigroup.mem_corner_iff idem).mp r.2).1
mul_one r := Subtype.ext ((Subsemigroup.mem_corner_iff idem).mp r.2).2
