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

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

@[deprecated add_div (since := "2025-08-25")]

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

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

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

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

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

theorem inv_add_inv' {K : Type u_1} [DivisionSemiring K] {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ + b⁻¹ = a⁻¹ * (a + b) * b⁻¹

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

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

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

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

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

theorem Commute.div_add_div {K : Type u_1} [DivisionSemiring K] {a b c d : K} (hbc : Commute b c) (hbd : Commute b d) (hb : b ≠ 0) (hd : d ≠ 0) : a / b + c / d = (a * d + b * c) / (b * d)

theorem Commute.one_div_add_one_div {K : Type u_1} [DivisionSemiring K] {a b : K} (hab : Commute a b) (ha : a ≠ 0) (hb : b ≠ 0) : 1 / a + 1 / b = (a + b) / (a * b)

theorem Commute.inv_add_inv {K : Type u_1} [DivisionSemiring K] {a b : K} (hab : Commute a b) (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ + b⁻¹ = (a + b) / (a * b)

@[simp]

theorem add_self_div_two {K : Type u_1} [DivisionSemiring K] [NeZero 2] (a : K) : (a + a) / 2 = a

@[simp]

theorem add_halves {K : Type u_1} [DivisionSemiring K] [NeZero 2] (a : K) : a / 2 + a / 2 = a

@[simp]

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

@[simp]

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

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

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

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

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

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

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

theorem inv_sub_inv' {K : Type u_1} [DivisionRing K] {a 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.

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

theorem inv_eq_self₀ {K : Type u_1} [DivisionRing K] {a : K} : a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1

theorem self_eq_inv₀ {K : Type u_1} [DivisionRing K] {a : K} : a = a⁻¹ ↔ a = -1 ∨ a = 0 ∨ a = 1

@[instance 100]

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

theorem Commute.div_sub_div {K : Type u_1} [DivisionRing K] {a b c d : K} (hbc : Commute b c) (hbd : Commute b d) (hb : b ≠ 0) (hd : d ≠ 0) : a / b - c / d = (a * d - b * c) / (b * d)

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

theorem sub_half {K : Type u_1} [DivisionRing K] [NeZero 2] (a : K) : a - a / 2 = a / 2

theorem half_sub {K : Type u_1} [DivisionRing K] [NeZero 2] (a : K) : a / 2 - a = -(a / 2)

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

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

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

@[instance 100]

instance Field.toGrindField {K : Type u_1} [Field K] : Lean.Grind.Field K

theorem div_sub_div {K : Type u_1} [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)

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

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

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

@[instance 100]

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

@[reducible, inline]

noncomputable abbrev DivisionRing.ofIsUnitOrEqZero {R : Type u_3} [Nontrivial R] [Ring R] (h : ∀ (a : R), IsUnit a ∨ a = 0) : DivisionRing R

Constructs a DivisionRing structure on a Ring consisting only of units and 0.

@[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.

@[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 : 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) : DivisionSemiring K

Pullback a DivisionSemiring along an injective function.

@[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 : 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) : DivisionRing K

Pullback a DivisionSemiring along an injective function.

@[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 : 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) : Semifield K

Pullback a Field along an injective function.

@[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 : 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.

Order dual

instance OrderDual.instRatCast {K : Type u_1} [RatCast K] : RatCast Kᵒᵈ

instance OrderDual.instDivisionSemiring {K : Type u_1} [DivisionSemiring K] : DivisionSemiring Kᵒᵈ

instance OrderDual.instDivisionRing {K : Type u_1} [DivisionRing K] : DivisionRing Kᵒᵈ

instance OrderDual.instSemifield {K : Type u_1} [Semifield K] : Semifield Kᵒᵈ

instance OrderDual.instField {K : Type u_1} [Field K] : Field Kᵒᵈ

@[simp]

theorem toDual_ratCast {K : Type u_1} [RatCast K] (n : ℚ) : OrderDual.toDual ↑n = ↑n

@[simp]

theorem ofDual_ratCast {K : Type u_1} [RatCast K] (n : ℚ) : OrderDual.ofDual ↑n = ↑n

Lexicographic order

instance Lex.instRatCast {K : Type u_1} [RatCast K] : RatCast (Lex K)

instance Lex.instDivisionSemiring {K : Type u_1} [DivisionSemiring K] : DivisionSemiring (Lex K)

instance Lex.instDivisionRing {K : Type u_1} [DivisionRing K] : DivisionRing (Lex K)

instance Lex.instSemifield {K : Type u_1} [Semifield K] : Semifield (Lex K)

instance Lex.instField {K : Type u_1} [Field K] : Field (Lex K)

@[simp]

theorem toLex_ratCast {K : Type u_1} [RatCast K] (n : ℚ) : toLex ↑n = ↑n

@[simp]

theorem ofLex_ratCast {K : Type u_1} [RatCast K] (n : ℚ) : ofLex ↑n = ↑n