English
Let f: R → S be surjective and suppose R has a NonUnitalNonAssocCommRing structure. Then S inherits a NonUnitalNonAssocCommRing structure transported along f.
Русский
Пусть f: R → S — суръекция и R обладает структурой NonUnitalNonAssocCommRing. Тогда S наследует структуру NonUnitalNonAssocCommRing, перенесённую по f.
LaTeX
$$$\text{Pushforward}_{f}({\text{NonUnitalNonAssocCommRing}}\,R) = {\text{NonUnitalNonAssocCommRing}}\,S.$$$
Lean4
/-- Pushforward a `NonUnitalNonAssocCommRing` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalNonAssocCommRing [NonUnitalNonAssocCommRing 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) : NonUnitalNonAssocCommRing S
where
toNonUnitalNonAssocRing := hf.nonUnitalNonAssocRing f zero add mul neg sub nsmul zsmul
__ := hf.nonUnitalNonAssocCommSemiring f zero add mul nsmul
