English
If f: R → S is surjective and R has a NonUnitalSemiring structure with compatible operations, then S inherits a NonUnitalSemiring structure.
Русский
Если f: R → S сюръективна и R имеет структуру NonUnitalSemiring с совместимыми операциями, то S наследует NonUnitalSemiring.
LaTeX
$$$\\exists\\; \\mathcal{S}: \\text{NonUnitalSemiring}(S)$$$
Lean4
/-- Pushforward a `NonUnitalNonAssocSemiring` instance along a surjective function.
See note [reducible non-instances]. -/
protected abbrev nonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring 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) : NonUnitalNonAssocSemiring S
where
toAddCommMonoid := hf.addCommMonoid f zero add (swap nsmul)
__ := hf.distrib f add mul
__ := hf.mulZeroClass f zero mul
