Documentation

Mathlib.Algebra.Field.Basic

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

theorem add_div {K : Type u_1} [DivisionSemiring K] (a : K) (b : K) (c : K) :
(a + b) / c = a / c + b / c
theorem div_add_div_same {K : Type u_1} [DivisionSemiring K] (a : K) (b : K) (c : K) :
a / c + b / c = (a + b) / c
theorem same_add_div {K : Type u_1} [DivisionSemiring K] {a : K} {b : K} (h : b 0) :
(b + a) / b = 1 + a / b
theorem div_add_same {K : Type u_1} [DivisionSemiring K] {a : K} {b : K} (h : b 0) :
(a + b) / b = a / b + 1
theorem one_add_div {K : Type u_1} [DivisionSemiring K] {a : K} {b : K} (h : b 0) :
1 + a / b = (b + a) / b
theorem div_add_one {K : Type u_1} [DivisionSemiring K] {a : K} {b : K} (h : b 0) :
a / b + 1 = (a + b) / b
theorem inv_add_inv' {K : Type u_1} [DivisionSemiring K] {a : K} {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 : K} {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 : K) (b : K) (hc : c 0) :
a + b / c = (a * c + b) / c
theorem add_div' {K : Type u_1} [DivisionSemiring K] (a : K) (b : K) (c : K) (hc : c 0) :
b + a / c = (b * c + a) / c
theorem div_add' {K : Type u_1} [DivisionSemiring K] (a : K) (b : K) (c : K) (hc : c 0) :
a / c + b = (a + b * c) / c
theorem Commute.div_add_div {K : Type u_1} [DivisionSemiring K] {a : K} {b : K} {c : K} {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 : K} {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 : K} {b : K} (hab : Commute a b) (ha : a 0) (hb : b 0) :
a⁻¹ + b⁻¹ = (a + b) / (a * b)
theorem one_div_neg_eq_neg_one_div {K : Type u_1} [DivisionMonoid K] [HasDistribNeg K] (a : K) :
1 / -a = -(1 / a)
theorem div_neg_eq_neg_div {K : Type u_1} [DivisionMonoid K] [HasDistribNeg K] (a : K) (b : K) :
b / -a = -(b / a)
theorem neg_div {K : Type u_1} [DivisionMonoid K] [HasDistribNeg K] (a : K) (b : K) :
-b / a = -(b / a)
theorem neg_div' {K : Type u_1} [DivisionMonoid K] [HasDistribNeg K] (a : K) (b : K) :
-(b / a) = -b / a
@[simp]
theorem neg_div_neg_eq {K : Type u_1} [DivisionMonoid K] [HasDistribNeg K] (a : K) (b : K) :
-a / -b = a / b
theorem neg_inv {K : Type u_1} [DivisionMonoid K] [HasDistribNeg K] {a : K} :
theorem div_neg {K : Type u_1} [DivisionMonoid K] [HasDistribNeg K] {b : K} (a : K) :
a / -b = -(a / b)
theorem inv_neg {K : Type u_1} [DivisionMonoid K] [HasDistribNeg K] {a : K} :
theorem inv_neg_one {K : Type u_1} [DivisionMonoid K] [HasDistribNeg K] :
(-1)⁻¹ = -1
@[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 : K) (b : K) (c : K) :
a / c - b / c = (a - b) / c
theorem same_sub_div {K : Type u_1} [DivisionRing K] {a : K} {b : K} (h : b 0) :
(b - a) / b = 1 - a / b
theorem one_sub_div {K : Type u_1} [DivisionRing K] {a : K} {b : K} (h : b 0) :
1 - a / b = (b - a) / b
theorem div_sub_same {K : Type u_1} [DivisionRing K] {a : K} {b : K} (h : b 0) :
(a - b) / b = a / b - 1
theorem div_sub_one {K : Type u_1} [DivisionRing K] {a : K} {b : K} (h : b 0) :
a / b - 1 = (a - b) / b
theorem sub_div {K : Type u_1} [DivisionRing K] (a : K) (b : K) (c : K) :
(a - b) / c = a / c - b / c
theorem inv_sub_inv' {K : Type u_1} [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.

theorem one_div_mul_sub_mul_one_div_eq_one_div_add_one_div {K : Type u_1} [DivisionRing K] {a : K} {b : K} (ha : a 0) (hb : b 0) :
1 / a * (b - a) * (1 / b) = 1 / a - 1 / b
@[instance 100]
Equations
  • =
theorem Commute.div_sub_div {K : Type u_1} [DivisionRing K] {a : K} {b : K} {c : K} {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 : K} {b : K} (hab : Commute a b) (ha : a 0) (hb : b 0) :
a⁻¹ - b⁻¹ = (b - a) / (a * b)
theorem div_add_div {K : Type u_1} [Semifield K] {b : K} {d : K} (a : K) (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 : K} {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 : K} {b : K} (ha : a 0) (hb : b 0) :
a⁻¹ + b⁻¹ = (a + b) / (a * b)
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 : K} {b : K} (ha : a 0) (hb : b 0) :
a⁻¹ - b⁻¹ = (b - a) / (a * b)
theorem sub_div' {K : Type u_1} [Field K] (a : K) (b : K) (c : K) (hc : c 0) :
b - a / c = (b * c - a) / c
theorem div_sub' {K : Type u_1} [Field K] (a : K) (b : K) (c : K) (hc : c 0) :
a / c - b = (a - c * b) / c
@[instance 100]
instance Field.isDomain {K : Type u_1} [Field K] :
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
Instances For
    @[reducible, inline]
    noncomputable abbrev Field.ofIsUnitOrEqZero {R : Type u_3} [Nontrivial R] [CommRing R] (h : ∀ (a : R), IsUnit a a = 0) :

    Constructs a Field structure on a CommRing consisting only of units and 0.

    Equations
    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 : KL) (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 : KL) (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 : KL) (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
          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 : KL) (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) :

            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.instRatCast = inst
              Equations
              • OrderDual.instDivisionSemiring = inst
              Equations
              • OrderDual.instDivisionRing = inst
              Equations
              • OrderDual.instSemifield = inst
              instance OrderDual.instField {K : Type u_1} [Field K] :
              Equations
              • OrderDual.instField = inst
              @[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] :
              Equations
              • Lex.instRatCast = inst
              Equations
              • Lex.instDivisionSemiring = inst
              Equations
              • Lex.instDivisionRing = inst
              instance Lex.instSemifield {K : Type u_1} [Semifield K] :
              Equations
              • Lex.instSemifield = inst
              instance Lex.instField {K : Type u_1} [Field K] :
              Equations
              • Lex.instField = inst
              @[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