toCommSemiring — Mathlib

English

A subsemiring of a CommSemiring is a CommSemiring.

Русский

Подполугольник из коммутативного полукольца сам является коммутативным полукольцом.

LaTeX

$$$\forall {R} [\text{CommSemiring } R] (s : \mathrm{Subsemiring}(R)), \mathrm{CommSemiring}(s)$$$

Lean4

/-- A subsemiring of a `CommSemiring` is a `CommSemiring`. -/
instance toCommSemiring {R} [CommSemiring R] (s : Subsemiring R) : CommSemiring s :=
  { s.toSemiring with mul_comm := fun _ _ => Subtype.eq <| mul_comm _ _ }

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