Lemmas about division (semi)rings and (semi)fields #
@[simp]
@[instance 100]
Equations
- ⋯ = ⋯
theorem
RingHom.injective
{K : Type u_1}
{L : Type u_2}
[DivisionRing K]
[Semiring L]
[Nontrivial L]
(f : K →+* L)
:
@[reducible, inline]
noncomputable abbrev
DivisionRing.ofIsUnitOrEqZero
{R : Type u_3}
[Nontrivial R]
[Ring R]
(h : ∀ (a : R), IsUnit a ∨ a = 0)
:
Constructs a DivisionRing
structure on a Ring
consisting only of units and 0.
Equations
- DivisionRing.ofIsUnitOrEqZero h = DivisionRing.mk ⋯ GroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (q : ℚ≥0) => HMul.hMul ↑q) ⋯ ⋯ (fun (q : ℚ) => HMul.hMul ↑q) ⋯
Instances For
@[reducible, inline]
noncomputable abbrev
Field.ofIsUnitOrEqZero
{R : Type u_3}
[Nontrivial R]
[CommRing R]
(h : ∀ (a : R), IsUnit a ∨ a = 0)
:
Field R
Constructs a Field
structure on a CommRing
consisting only of units and 0.
Equations
- Field.ofIsUnitOrEqZero h = Field.mk ⋯ DivisionRing.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionRing.nnqsmul ⋯ ⋯ DivisionRing.qsmul ⋯
Instances For
@[reducible, inline]
abbrev
Function.Injective.divisionSemiring
{K : Type u_1}
{L : Type u_2}
[Zero K]
[Add K]
[One K]
[Mul K]
[Inv K]
[Div K]
[SMul ℕ K]
[SMul ℚ≥0 K]
[Pow K ℕ]
[Pow K ℤ]
[NatCast K]
[NNRatCast K]
(f : K → L)
(hf : Function.Injective f)
[DivisionSemiring L]
(zero : f 0 = 0)
(one : f 1 = 1)
(add : ∀ (x y : K), f (x + y) = f x + f y)
(mul : ∀ (x y : K), f (x * y) = f x * f y)
(inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹)
(div : ∀ (x y : K), f (x / y) = f x / f y)
(nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x)
(nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x)
(npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n)
(natCast : ∀ (n : ℕ), f ↑n = ↑n)
(nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q)
:
Pullback a DivisionSemiring
along an injective function.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
Function.Injective.divisionRing
{K : Type u_1}
{L : Type u_2}
[Zero K]
[Add K]
[Neg K]
[Sub K]
[One K]
[Mul K]
[Inv K]
[Div K]
[SMul ℕ K]
[SMul ℤ K]
[SMul ℚ≥0 K]
[SMul ℚ K]
[Pow K ℕ]
[Pow K ℤ]
[NatCast K]
[IntCast K]
[NNRatCast K]
[RatCast K]
(f : K → L)
(hf : Function.Injective f)
[DivisionRing L]
(zero : f 0 = 0)
(one : f 1 = 1)
(add : ∀ (x y : K), f (x + y) = f x + f y)
(mul : ∀ (x y : K), f (x * y) = f x * f y)
(neg : ∀ (x : K), f (-x) = -f x)
(sub : ∀ (x y : K), f (x - y) = f x - f y)
(inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹)
(div : ∀ (x y : K), f (x / y) = f x / f y)
(nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x)
(zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x)
(nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x)
(qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x)
(npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : K) (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)
:
Pullback a DivisionSemiring
along an injective function.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
Function.Injective.semifield
{K : Type u_1}
{L : Type u_2}
[Zero K]
[Add K]
[One K]
[Mul K]
[Inv K]
[Div K]
[SMul ℕ K]
[SMul ℚ≥0 K]
[Pow K ℕ]
[Pow K ℤ]
[NatCast K]
[NNRatCast K]
(f : K → L)
(hf : Function.Injective f)
[Semifield L]
(zero : f 0 = 0)
(one : f 1 = 1)
(add : ∀ (x y : K), f (x + y) = f x + f y)
(mul : ∀ (x y : K), f (x * y) = f x * f y)
(inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹)
(div : ∀ (x y : K), f (x / y) = f x / f y)
(nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x)
(nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x)
(npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n)
(natCast : ∀ (n : ℕ), f ↑n = ↑n)
(nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q)
:
Pullback a Field
along an injective function.
Equations
- Function.Injective.semifield f hf zero one add mul inv div nsmul nnqsmul npow zpow natCast nnratCast = Semifield.mk ⋯ CommGroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionSemiring.nnqsmul ⋯
Instances For
@[reducible, inline]
abbrev
Function.Injective.field
{K : Type u_1}
{L : Type u_2}
[Zero K]
[Add K]
[Neg K]
[Sub K]
[One K]
[Mul K]
[Inv K]
[Div K]
[SMul ℕ K]
[SMul ℤ K]
[SMul ℚ≥0 K]
[SMul ℚ K]
[Pow K ℕ]
[Pow K ℤ]
[NatCast K]
[IntCast K]
[NNRatCast K]
[RatCast K]
(f : K → L)
(hf : Function.Injective f)
[Field L]
(zero : f 0 = 0)
(one : f 1 = 1)
(add : ∀ (x y : K), f (x + y) = f x + f y)
(mul : ∀ (x y : K), f (x * y) = f x * f y)
(neg : ∀ (x : K), f (-x) = -f x)
(sub : ∀ (x y : K), f (x - y) = f x - f y)
(inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹)
(div : ∀ (x y : K), f (x / y) = f x / f y)
(nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x)
(zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x)
(nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x)
(qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x)
(npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : K) (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)
:
Field K
Pullback a Field
along an injective function.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Order dual #
Equations
- OrderDual.instDivisionSemiring = inst
Equations
- OrderDual.instDivisionRing = inst
Lexicographic order #
Equations
- Lex.instDivisionSemiring = inst
Equations
- Lex.instDivisionRing = inst