English
Pull back a DivisionSemiring structure along an injective function f: K → L, preserving zero, one, addition, multiplication, and division.
Русский
Вытягивает структуру DivisionSemiring через инъективное отображение f: K → L, сохраняющую нуль, единицу, сложение, умножение и деление.
LaTeX
$$$\\text{Pullback divisionSemiring along } f:\\ K \\to L$$$
Lean4
/-- Pullback a `DivisionSemiring` along an injective function. -/
-- See note [reducible non-instances]
protected abbrev divisionSemiring [DivisionSemiring 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) (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)
(nnqsmul : ∀ (q : ℚ≥0) (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) (nnratCast : ∀ q : ℚ≥0, f q = q) :
DivisionSemiring K where
toSemiring := hf.semiring f zero one add mul nsmul npow natCast
__ := hf.groupWithZero f zero one mul inv div npow zpow
nnratCast_def q := hf <| by rw [nnratCast, NNRat.cast_def, div, natCast, natCast]
nnqsmul := (· • ·)
nnqsmul_def q a := hf <| by rw [nnqsmul, NNRat.smul_def, mul, nnratCast]
