English
Let f: S → R be injective. If R has a NonUnitalNonAssocCommRing structure, then S inherits a NonUnitalNonAssocCommRing structure via pullback along f, with all the required additive, multiplicative, and negation operations preserved by f.
Русский
Пусть f: S → R инъективна. Если R обладает структурой NonUnitalNonAssocCommRing, то S наследует её через перенос по f, сохраняя аддитивность, умножение и отрицание.
LaTeX
$$$\\exists\\, \\mathcal{S}: \\text{NonUnitalNonAssocCommRing}(S),\\quad f(0)=0,\\quad \\forall x,y, f(x+y)=f(x)+f(y),\\quad \\forall x,y, f(x\\cdot y)=f(x)\\cdot f(y),\\quad \\forall x, f(-x)=-f(x).$$$
Lean4
/-- Pullback a `NonUnitalNonAssocCommRing` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalNonAssocCommRing [NonUnitalNonAssocCommRing R] (f : S → R) (hf : Injective f) (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
