English
Let R be a commutative semiring and X a type. The free algebra FreeAlgebra R X carries a canonical semiring structure extending the base ring structure, with the injections ι and the natural casting from R.
Русский
Пусть R — коммутативное полукольцо и X — множество. Свободная алгебра FreeAlgebra R X имеет естественную структуру полукольца, которая расширяет структуру базового кольца, вместе с инъекциями ι и естественным отображением из R.
LaTeX
$$$\mathrm{FreeAlgebra}(R,X)$ is a Semiring with the induced addition, multiplication, zero, one, and the (natural) cast from $R$.$$
Lean4
instance : Semiring (FreeAlgebra R X) where
__ := instMonoidWithZero R X
__ := instAddCommMonoid R X
__ := instDistrib R X
natCast n := Quot.mk _ (n : R)
natCast_zero := by simp; rfl
natCast_succ n := by simpa using Quot.sound Rel.add_scalar
