English
Let f: S → R be injective. If R has a CommSemiring structure, then S inherits a CommSemiring structure pulled back along f, with the necessary preservation of 0, 1, +, and ×.
Русский
Пусть f: S → R инъективна. Если R обладает структурой CommSemiring, то S наследует её через перенос по f.
LaTeX
$$$\\exists\\, \\mathcal{S}: \\text{CommSemiring}(S),\\quad f(0)=0,\\quad f(1)=1,\\quad \\forall x,y, f(x+y)=f(x)+f(y),\\quad \\forall x,y, f(x\\cdot y)=f(x)\\cdot f(y).$$$
Lean4
/-- Pullback a `CommSemiring` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev commSemiring [CommSemiring R] (zero : f 0 = 0) (one : f 1 = 1) (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)
(npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n) : CommSemiring S
where
toSemiring := hf.semiring f zero one add mul nsmul npow natCast
__ := hf.commSemigroup f mul
