English
Let f: S → R be surjective. If R is a Ring, then S inherits a Ring structure via surjective transfer.
Русский
Пусть f: S → R сюръективна. Если R является кольцом, то S наследует структуру кольца по сюръективному переносу.
LaTeX
$$$\\exists\\; \\mathcal{S}: \\text{Ring}(S)$$$
Lean4
/-- Pushforward a `NonAssocSemiring` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev nonAssocSemiring [NonAssocSemiring 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) (natCast : ∀ n : ℕ, f n = n) : NonAssocSemiring S
where
toNonUnitalNonAssocSemiring := hf.nonUnitalNonAssocSemiring f zero add mul nsmul
__ := hf.mulZeroOneClass f zero one mul
__ := hf.addMonoidWithOne f zero one add nsmul natCast
