English
Let f: S → R be injective. If R has a NonAssocRing structure (with +, ×, 0, neg, sub, etc.), then S inherits a NonAssocRing structure by pullback along f, preserving the ring operations via f.
Русский
Пусть f: S → R инъективна. Если R обладает структурой NonAssocRing, то S получает такую же структуру через перенос по f, сохраняя операции.
LaTeX
$$$\\exists\\, \\mathcal{S}: \\text{NonAssocRing}(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),\\quad \\forall x,y, f(x-y)=f(x)-f(y),\\quad \\forall n,x, f(n\\cdot x)=n\\cdot f(x),\\quad \\forall n,m, f(n+m)=f(n)+f(m).$$$
Lean4
/-- Pullback a `NonAssocRing` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev nonAssocRing [NonAssocRing 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) (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)
(natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) : NonAssocRing S
where
toNonUnitalNonAssocRing := hf.nonUnitalNonAssocRing f zero add mul neg sub nsmul zsmul
__ := hf.nonAssocSemiring f zero one add mul nsmul natCast
__ := hf.addCommGroupWithOne f zero one add neg sub nsmul zsmul natCast intCast
