English
If f: R → S is surjective and R has a NonUnitalNonAssocRing structure, then S inherits a NonUnitalNonAssocRing structure.
Русский
Если f: R → S сюръективна и R имеет структуру NonUnitalNonAssocRing, то S наследует её.
LaTeX
$$$\\exists\\; \\mathcal{S}: \\text{NonUnitalNonAssocRing}(S)$$$
Lean4
/-- Pushforward a `Semiring` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev semiring [Semiring 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) : Semiring S
where
toNonUnitalSemiring := hf.nonUnitalSemiring f zero add mul nsmul
__ := hf.nonAssocSemiring f zero one add mul nsmul natCast
__ := hf.monoidWithZero f zero one mul npow
