English
The set of languages forms a semiring with addition given by union and multiplication by concatenation, with zero as empty language and one as language containing the empty word; the usual ring-like axioms hold.
Русский
Множество языков образует полусемиринг: сложение — объединение, умножение — конкатенация; ноль — пустой язык, единица — язык, содержащий пустое слово; выполняются соответствующие аксиомы.
LaTeX
$$$ \operatorname{Semiring}(\text{Language } \alpha). $$$
Lean4
instance instSemiring : Semiring (Language α) where
add := (· + ·)
add_assoc := union_assoc
zero := 0
zero_add := empty_union
add_zero := union_empty
add_comm := union_comm
mul := (· * ·)
mul_assoc _ _ _ := image2_assoc append_assoc
zero_mul _ := image2_empty_left
mul_zero _ := image2_empty_right
one := 1
one_mul l := by simp [mul_def, one_def]
mul_one l := by simp [mul_def, one_def]
natCast n := if n = 0 then 0 else 1
natCast_zero := rfl
natCast_succ n := by cases n <;> simp [add_def, zero_def]
left_distrib _ _ _ := image2_union_right
right_distrib _ _ _ := image2_union_left
nsmul := nsmulRec
