English
Let f: S → R be injective. If R has a NonUnitalNonAssocCommSemiring structure, then S inherits a compatible NonUnitalNonAssocCommSemiring structure via pullback along f, with f preserving addition and multiplication and scalar actions.
Русский
Пусть f: S → R инъективна. Если R имеет структуру NonUnitalNonAssocCommSemiring, то S наследует совместную структуру через перенос по f, сохраняя сложение, умножение и действия на скаляры.
LaTeX
$$$\\exists\\, \\mathcal{S}: \\text{NonUnitalNonAssocCommSemiring}(S),\\quad f(0)=0,\\quad \\forall x,y, f(x+y)=f(x)+f(y),\\quad \\forall x,y, f(x\\cdot y)=f(x)\\cdot f(y),\\quad \\forall n, f(n\\cdot x)=n\\cdot f(x).$$$
Lean4
/-- Pullback a `NonUnitalNonAssocCommSemiring` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalNonAssocCommSemiring [NonUnitalNonAssocCommSemiring R] (zero : f 0 = 0)
(add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
(nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) : NonUnitalNonAssocCommSemiring S
where
toNonUnitalNonAssocSemiring := hf.nonUnitalNonAssocSemiring f zero add mul nsmul
__ := hf.commMagma f mul
