instNonUnitalSubsemiringClassIdeal

English

Any ideal I of a semiring R forms a non-unital subsemiring of R, since ab ∈ I whenever a,b ∈ I.

Русский

Любой идеал I полугруппы R образует ненулевой подполусемиринг, так как произведение элементов идеала принадлежит идеалу.

LaTeX

$$If a,b ∈ I then ab ∈ I$$

Lean4

instance {R} [Semiring R] : NonUnitalSubsemiringClass (Ideal R) R where mul_mem _ hb := Ideal.mul_mem_left _ _ hb

Похожие утверждения