English
If f: K → L is injective and L is a DivisionRing with preserved operations, then K inherits a DivisionRing structure via pullback along f.
Русский
Если f: K → L инъективно и L — делительный кольцо с сохранением операций, то K наследует структуру делительного кольца через вытягивание по f.
LaTeX
$$$\\exists$ DivisionRing K such that $f$ is a homomorphism preserving operations$$
Lean4
/-- Pullback a `DivisionSemiring` along an injective function. -/
-- See note [reducible non-instances]
protected abbrev divisionRing [DivisionRing L] (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)
(inv : ∀ x, f x⁻¹ = (f x)⁻¹) (div : ∀ 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) (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x)
(qsmul : ∀ (q : ℚ) (x), f (q • x) = q • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n)
(nnratCast : ∀ q : ℚ≥0, f q = q) (ratCast : ∀ q : ℚ, f q = q) : DivisionRing K
where
toRing := hf.ring f zero one add mul neg sub nsmul zsmul npow natCast intCast
__ := hf.groupWithZero f zero one mul inv div npow zpow
__ := hf.divisionSemiring f zero one add mul inv div nsmul nnqsmul npow zpow natCast nnratCast
ratCast_def q := hf <| by rw [ratCast, div, intCast, natCast, Rat.cast_def]
qsmul := (· • ·)
qsmul_def q a := hf <| by rw [qsmul, mul, Rat.smul_def, ratCast]
