English
Let f: S → R be surjective. If R has a NonUnitalRing structure, then S inherits a NonUnitalRing structure through f.
Русский
Пусть f: S → R сюръективна. Если R имеет NonUnitalRing, то S наследует его через f.
LaTeX
$$$\\exists\\; \\mathcal{S}: \\text{NonUnitalRing}(S)$$$
Lean4
/-- Pushforward a `NonUnitalNonAssocRing` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalNonAssocRing [NonUnitalNonAssocRing 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) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
(nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) : NonUnitalNonAssocRing S
where
toAddCommGroup := hf.addCommGroup f zero add neg sub (swap nsmul) (swap zsmul)
__ := hf.nonUnitalNonAssocSemiring f zero add mul nsmul
