English
As above, with explicit expressions for 0, +, and × preserved by f.
Русский
Аналогично, с явным сохранением 0, +, × через f.
LaTeX
$$$\\exists\\; \\mathcal{S}: \\text{NonUnitalSemiring}(S),\\; f(0)=0,\\; \\forall x,y, f(x+y)=f(x)+f(y),\\; \\forall x,y, f(x\\cdot y)=f(x)\\cdot f(y).$$$
Lean4
/-- Pushforward a `NonUnitalSemiring` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalSemiring [NonUnitalSemiring 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) : NonUnitalSemiring S
where
toNonUnitalNonAssocSemiring := hf.nonUnitalNonAssocSemiring f zero add mul nsmul
__ := hf.semigroupWithZero f zero mul
