Lemmas about division (semi)rings and (semi)fields #
theorem
one_div_neg_one_eq_neg_one
{K : Type u_1}
[inst : DivisionMonoid K]
[inst : HasDistribNeg K]
:
theorem
one_div_neg_eq_neg_one_div
{K : Type u_1}
[inst : DivisionMonoid K]
[inst : HasDistribNeg K]
(a : K)
:
theorem
div_neg_eq_neg_div
{K : Type u_1}
[inst : DivisionMonoid K]
[inst : HasDistribNeg K]
(a : K)
(b : K)
:
theorem
neg_div_neg_eq
{K : Type u_1}
[inst : DivisionMonoid K]
[inst : HasDistribNeg K]
(a : K)
(b : K)
:
@[simp]
@[simp]
Equations
theorem
RingHom.injective
{α : Type u_1}
{β : Type u_2}
[inst : DivisionRing α]
[inst : Semiring β]
[inst : Nontrivial β]
(f : α →+* β)
:
noncomputable def
divisionRingOfIsUnitOrEqZero
{R : Type u_1}
[inst : Nontrivial R]
[hR : Ring R]
(h : ∀ (a : R), IsUnit a ∨ a = 0)
:
Constructs a DivisionRing
structure on a Ring
consisting only of units and 0.
Equations
- divisionRingOfIsUnitOrEqZero h = let src := groupWithZeroOfIsUnitOrEqZero h; DivisionRing.mk GroupWithZero.zpow (_ : ∀ (a : R), a ≠ 0 → a * a⁻¹ = 1) (_ : 0⁻¹ = 0) (qsmulRec Rat.cast)
noncomputable def
fieldOfIsUnitOrEqZero
{R : Type u_1}
[inst : Nontrivial R]
[hR : CommRing R]
(h : ∀ (a : R), IsUnit a ∨ a = 0)
:
Field R
Constructs a Field
structure on a CommRing
consisting only of units and 0.
See note [reducible non-instances].
def
Function.Injective.divisionSemiring
{α : Type u_1}
{β : Type u_2}
[inst : DivisionSemiring β]
[inst : Zero α]
[inst : Mul α]
[inst : Add α]
[inst : One α]
[inst : Inv α]
[inst : Div α]
[inst : SMul ℕ α]
[inst : Pow α ℕ]
[inst : Pow α ℤ]
[inst : NatCast α]
(f : α → β)
(hf : Function.Injective f)
(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 : ∀ (x : α) (n : ℕ), f (n • x) = n • f x)
(npow : ∀ (x : α) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : α) (n : ℤ), f (x ^ n) = f x ^ n)
(nat_cast : ∀ (n : ℕ), f ↑n = ↑n)
:
Pullback a DivisionSemiring
along an injective function.
Equations
- One or more equations did not get rendered due to their size.
def
Function.Injective.divisionRing
{K : Type u_1}
[inst : DivisionRing K]
{K' : Type u_2}
[inst : Zero K']
[inst : One K']
[inst : Add K']
[inst : Mul K']
[inst : Neg K']
[inst : Sub K']
[inst : Inv K']
[inst : Div K']
[inst : SMul ℕ K']
[inst : SMul ℤ K']
[inst : SMul ℚ K']
[inst : Pow K' ℕ]
[inst : Pow K' ℤ]
[inst : NatCast K']
[inst : IntCast K']
[inst : RatCast K']
(f : K' → K)
(hf : Function.Injective f)
(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 : ∀ (x : K') (n : ℕ), f (n • x) = n • f x)
(zsmul : ∀ (x : K') (n : ℤ), f (n • x) = n • f x)
(qsmul : ∀ (x : K') (n : ℚ), f (n • x) = n • f x)
(npow : ∀ (x : K') (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : K') (n : ℤ), f (x ^ n) = f x ^ n)
(nat_cast : ∀ (n : ℕ), f ↑n = ↑n)
(int_cast : ∀ (n : ℤ), f ↑n = ↑n)
(rat_cast : ∀ (n : ℚ), f ↑n = ↑n)
:
DivisionRing K'
Pullback a DivisionSemiring
along an injective function.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
def
Function.Injective.semifield
{α : Type u_1}
{β : Type u_2}
[inst : Semifield β]
[inst : Zero α]
[inst : Mul α]
[inst : Add α]
[inst : One α]
[inst : Inv α]
[inst : Div α]
[inst : SMul ℕ α]
[inst : Pow α ℕ]
[inst : Pow α ℤ]
[inst : NatCast α]
(f : α → β)
(hf : Function.Injective f)
(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 : ∀ (x : α) (n : ℕ), f (n • x) = n • f x)
(npow : ∀ (x : α) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : α) (n : ℤ), f (x ^ n) = f x ^ n)
(nat_cast : ∀ (n : ℕ), f ↑n = ↑n)
:
Pullback a Field
along an injective function.
Equations
- One or more equations did not get rendered due to their size.
def
Function.Injective.field
{K : Type u_1}
[inst : Field K]
{K' : Type u_2}
[inst : Zero K']
[inst : Mul K']
[inst : Add K']
[inst : Neg K']
[inst : Sub K']
[inst : One K']
[inst : Inv K']
[inst : Div K']
[inst : SMul ℕ K']
[inst : SMul ℤ K']
[inst : SMul ℚ K']
[inst : Pow K' ℕ]
[inst : Pow K' ℤ]
[inst : NatCast K']
[inst : IntCast K']
[inst : RatCast K']
(f : K' → K)
(hf : Function.Injective f)
(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 : ∀ (x : K') (n : ℕ), f (n • x) = n • f x)
(zsmul : ∀ (x : K') (n : ℤ), f (n • x) = n • f x)
(qsmul : ∀ (x : K') (n : ℚ), f (n • x) = n • f x)
(npow : ∀ (x : K') (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : K') (n : ℤ), f (x ^ n) = f x ^ n)
(nat_cast : ∀ (n : ℕ), f ↑n = ↑n)
(int_cast : ∀ (n : ℤ), f ↑n = ↑n)
(rat_cast : ∀ (n : ℚ), f ↑n = ↑n)
:
Field K'
Pullback a Field
along an injective function.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Order dual #
Equations
- instDivisionSemiringOrderDual = h
Equations
- instDivisionRingOrderDual = h
Lexicographic order #
Equations
- instDivisionSemiringLex = h
Equations
- instDivisionRingLex = h