Lemmas about division (semi)rings and (semi)fields

ink

theorem add_div {α : Type u_1} [inst : DivisionSemiring α] (a : α) (b : α) (c : α) : (a + b) / c = a / c + b / c

ink

theorem div_add_div_same {α : Type u_1} [inst : DivisionSemiring α] (a : α) (b : α) (c : α) : a / c + b / c = (a + b) / c

ink

theorem same_add_div {α : Type u_1} [inst : DivisionSemiring α] {a : α} {b : α} (h : b ≠ 0) : (b + a) / b = 1 + a / b

ink

theorem div_add_same {α : Type u_1} [inst : DivisionSemiring α] {a : α} {b : α} (h : b ≠ 0) : (a + b) / b = a / b + 1

ink

theorem one_add_div {α : Type u_1} [inst : DivisionSemiring α] {a : α} {b : α} (h : b ≠ 0) : 1 + a / b = (b + a) / b

ink

theorem div_add_one {α : Type u_1} [inst : DivisionSemiring α] {a : α} {b : α} (h : b ≠ 0) : a / b + 1 = (a + b) / b

ink

theorem one_div_mul_add_mul_one_div_eq_one_div_add_one_div {α : Type u_1} [inst : DivisionSemiring α] {a : α} {b : α} (ha : a ≠ 0) (hb : b ≠ 0) : 1 / a * (a + b) * (1 / b) = 1 / a + 1 / b

ink

theorem add_div_eq_mul_add_div {α : Type u_1} [inst : DivisionSemiring α] {c : α} (a : α) (b : α) (hc : c ≠ 0) : a + b / c = (a * c + b) / c

ink

theorem add_div' {α : Type u_1} [inst : DivisionSemiring α] (a : α) (b : α) (c : α) (hc : c ≠ 0) : b + a / c = (b * c + a) / c

ink

theorem div_add' {α : Type u_1} [inst : DivisionSemiring α] (a : α) (b : α) (c : α) (hc : c ≠ 0) : a / c + b = (a + b * c) / c

ink

theorem one_div_neg_one_eq_neg_one {K : Type u_1} [inst : DivisionMonoid K] [inst : HasDistribNeg K] : 1 / -1 = -1

ink

theorem one_div_neg_eq_neg_one_div {K : Type u_1} [inst : DivisionMonoid K] [inst : HasDistribNeg K] (a : K) : 1 / -a = -(1 / a)

ink

theorem div_neg_eq_neg_div {K : Type u_1} [inst : DivisionMonoid K] [inst : HasDistribNeg K] (a : K) (b : K) : b / -a = -(b / a)

ink

theorem neg_div {K : Type u_1} [inst : DivisionMonoid K] [inst : HasDistribNeg K] (a : K) (b : K) : -b / a = -(b / a)

ink

theorem neg_div' {K : Type u_1} [inst : DivisionMonoid K] [inst : HasDistribNeg K] (a : K) (b : K) : -(b / a) = -b / a

ink

theorem neg_div_neg_eq {K : Type u_1} [inst : DivisionMonoid K] [inst : HasDistribNeg K] (a : K) (b : K) : -a / -b = a / b

ink

theorem neg_inv {K : Type u_1} [inst : DivisionMonoid K] [inst : HasDistribNeg K] {a : K} : -a⁻¹ = (-a)⁻¹

ink

theorem div_neg {K : Type u_1} [inst : DivisionMonoid K] [inst : HasDistribNeg K] {b : K} (a : K) : a / -b = -(a / b)

ink

theorem inv_neg {K : Type u_1} [inst : DivisionMonoid K] [inst : HasDistribNeg K] {a : K} : (-a)⁻¹ = -a⁻¹

ink

theorem inv_neg_one {K : Type u_1} [inst : DivisionMonoid K] [inst : HasDistribNeg K] : (-1)⁻¹ = -1

ink

@[simp]

theorem div_neg_self {K : Type u_1} [inst : DivisionRing K] {a : K} (h : a ≠ 0) : a / -a = -1

ink

@[simp]

theorem neg_div_self {K : Type u_1} [inst : DivisionRing K] {a : K} (h : a ≠ 0) : -a / a = -1

ink

theorem div_sub_div_same {K : Type u_1} [inst : DivisionRing K] (a : K) (b : K) (c : K) : a / c - b / c = (a - b) / c

ink

theorem same_sub_div {K : Type u_1} [inst : DivisionRing K] {a : K} {b : K} (h : b ≠ 0) : (b - a) / b = 1 - a / b

ink

theorem one_sub_div {K : Type u_1} [inst : DivisionRing K] {a : K} {b : K} (h : b ≠ 0) : 1 - a / b = (b - a) / b

ink

theorem div_sub_same {K : Type u_1} [inst : DivisionRing K] {a : K} {b : K} (h : b ≠ 0) : (a - b) / b = a / b - 1

ink

theorem div_sub_one {K : Type u_1} [inst : DivisionRing K] {a : K} {b : K} (h : b ≠ 0) : a / b - 1 = (a - b) / b

ink

theorem sub_div {K : Type u_1} [inst : DivisionRing K] (a : K) (b : K) (c : K) : (a - b) / c = a / c - b / c

ink

theorem inv_sub_inv' {K : Type u_1} [inst : DivisionRing K] {a : K} {b : K} (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ - b⁻¹ = a⁻¹ * (b - a) * b⁻¹

See inv_sub_inv for the more convenient version when K is commutative.

ink

theorem one_div_mul_sub_mul_one_div_eq_one_div_add_one_div {K : Type u_1} [inst : DivisionRing K] {a : K} {b : K} (ha : a ≠ 0) (hb : b ≠ 0) : 1 / a * (b - a) * (1 / b) = 1 / a - 1 / b

ink

instance DivisionRing.isDomain {K : Type u_1} [inst : DivisionRing K] : IsDomain K

Equations

• @DivisionRing.isDomain = @DivisionRing.isDomain.proof_1

ink

theorem div_add_div {α : Type u_1} [inst : Semifield α] {b : α} {d : α} (a : α) (c : α) (hb : b ≠ 0) (hd : d ≠ 0) : a / b + c / d = (a * d + b * c) / (b * d)

ink

theorem one_div_add_one_div {α : Type u_1} [inst : Semifield α] {a : α} {b : α} (ha : a ≠ 0) (hb : b ≠ 0) : 1 / a + 1 / b = (a + b) / (a * b)

ink

theorem inv_add_inv {α : Type u_1} [inst : Semifield α] {a : α} {b : α} (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ + b⁻¹ = (a + b) / (a * b)

ink

theorem div_sub_div {K : Type u_1} [inst : Field K] (a : K) {b : K} (c : K) {d : K} (hb : b ≠ 0) (hd : d ≠ 0) : a / b - c / d = (a * d - b * c) / (b * d)

ink

theorem inv_sub_inv {K : Type u_1} [inst : Field K] {a : K} {b : K} (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ - b⁻¹ = (b - a) / (a * b)

ink

theorem sub_div' {K : Type u_1} [inst : Field K] (a : K) (b : K) (c : K) (hc : c ≠ 0) : b - a / c = (b * c - a) / c

ink

theorem div_sub' {K : Type u_1} [inst : Field K] (a : K) (b : K) (c : K) (hc : c ≠ 0) : a / c - b = (a - c * b) / c

ink

instance Field.isDomain {K : Type u_1} [inst : Field K] : IsDomain K

Equations

• @Field.isDomain = @Field.isDomain.proof_1

ink

theorem RingHom.injective {α : Type u_1} {β : Type u_2} [inst : DivisionRing α] [inst : Semiring β] [inst : Nontrivial β] (f : α →+* β) : Function.Injective ↑f

ink

noncomputable def divisionRingOfIsUnitOrEqZero {R : Type u_1} [inst : Nontrivial R] [hR : Ring R] (h : ∀ (a : R), IsUnit a ∨ a = 0) : DivisionRing R

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)

ink

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].

Equations

• fieldOfIsUnitOrEqZero h = let src := groupWithZeroOfIsUnitOrEqZero h; Field.mk GroupWithZero.zpow (_ : ∀ (a : R), a ≠ 0 → a * a⁻¹ = 1) (_ : 0⁻¹ = 0) (qsmulRec Rat.cast)

ink

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) : DivisionSemiring α

Pullback a DivisionSemiring along an injective function.

Equations

• One or more equations did not get rendered due to their size.

ink

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.

ink

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) : Semifield α

Pullback a Field along an injective function.

Equations

• One or more equations did not get rendered due to their size.

ink

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

ink

instance instRatCastOrderDual {α : Type u_1} [h : RatCast α] : RatCast αᵒᵈ

Equations

• instRatCastOrderDual = h

ink

instance instDivisionSemiringOrderDual {α : Type u_1} [h : DivisionSemiring α] : DivisionSemiring αᵒᵈ

Equations

• instDivisionSemiringOrderDual = h

ink

instance instDivisionRingOrderDual {α : Type u_1} [h : DivisionRing α] : DivisionRing αᵒᵈ

Equations

• instDivisionRingOrderDual = h

ink

instance instSemifieldOrderDual {α : Type u_1} [h : Semifield α] : Semifield αᵒᵈ

Equations

• instSemifieldOrderDual = h

ink

instance instFieldOrderDual {α : Type u_1} [h : Field α] : Field αᵒᵈ

Equations

• instFieldOrderDual = h

ink

@[simp]

theorem toDual_rat_cast {α : Type u_1} [inst : RatCast α] (n : ℚ) : ↑OrderDual.toDual ↑n = ↑n

ink

@[simp]

theorem ofDual_rat_cast {α : Type u_1} [inst : RatCast α] (n : ℚ) : ↑(↑OrderDual.ofDual n) = ↑n

Lexicographic order

ink

instance instRatCastLex {α : Type u_1} [h : RatCast α] : RatCast (Lex α)

Equations

• instRatCastLex = h

ink

instance instDivisionSemiringLex {α : Type u_1} [h : DivisionSemiring α] : DivisionSemiring (Lex α)

Equations

• instDivisionSemiringLex = h

ink

instance instDivisionRingLex {α : Type u_1} [h : DivisionRing α] : DivisionRing (Lex α)

Equations

• instDivisionRingLex = h

ink

instance instSemifieldLex {α : Type u_1} [h : Semifield α] : Semifield (Lex α)

Equations

• instSemifieldLex = h

ink

instance instFieldLex {α : Type u_1} [h : Field α] : Field (Lex α)

Equations

• instFieldLex = h

ink

@[simp]

theorem toLex_rat_cast {α : Type u_1} [inst : RatCast α] (n : ℚ) : ↑toLex ↑n = ↑n

ink

@[simp]

theorem ofLex_rat_cast {α : Type u_1} [inst : RatCast α] (n : ℚ) : ↑(↑ofLex n) = ↑n