Theorems · Definition · field theory

Function.Injective.divisionRing

{K : Type u_1} →
  {L : Type u_2} →
    [inst : Zero K] →
      [inst_1 : Add K] →
        [inst_2 : Neg K] →
          [inst_3 : Sub K] →
            [inst_4 : One K] →
              [inst_5 : Mul K] →
                [inst_6 : Inv K] →
                  [inst_7 : Div K] →
                    [inst_8 : SMul ℕ K] →
                      [inst_9 : SMul ℤ K] →
                        [inst_10 : SMul ℚ≥0 K] →
                          [inst_11 : SMul ℚ K] →
                            [inst_12 : Pow K ℕ] →
                              [inst_13 : Pow K ℤ] →
                                [inst_14 : NatCast K] →
                                  [inst_15 : IntCast K] →
                                    [inst_16 : NNRatCast K] →
                                      [inst_17 : RatCast K] →
                                        (f : K → L) →
                                          Function.Injective f →
                                            [inst_18 : DivisionRing L] →
                                              f 0 = 0 →
                                                f 1 = 1 →
                                                  (∀ (x y : K), f (x + y) = f x + f y) →
                                                    (∀ (x y : K), f (x * y) = f x * f y) →
                                                      (∀ (x : K), f (-x) = -f x) →
                                                        (∀ (x y : K), f (x - y) = f x - f y) →
                                                          (∀ (x : K), f x⁻¹ = (f x)⁻¹) →
                                                            (∀ (x y : K), f (x / y) = f x / f y) →
                                                              (∀ (n : ℕ) (x : K), f (n • x) = n • f x) →
                                                                (∀ (n : ℤ) (x : K), f (n • x) = n • f x) →
                                                                  (∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x) →
                                                                    (∀ (q : ℚ) (x : K), f (q • x) = q • f x) →
                                                                      (∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n) →
                                                                        (∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n) →
                                                                          (∀ (n : ℕ), f ↑n = ↑n) →
                                                                            (∀ (n : ℤ), f ↑n = ↑n) →
                                                                              (∀ (q : ℚ≥0), f ↑q = ↑q) →
                                                                                (∀ (q : ℚ), f ↑q = ↑q) → DivisionRing K

Pullback a DivisionSemiring along an injective function.

Defined in

Mathlib.Algebra.Field.Basic

Cited by

0 results in Mathlib

Foundations

Depth 48 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

ZeroAddNegSubOneMulInvDivSMulSMulSMulSMulPowPowNatCastIntCastNNRatCastRatCastDivisionRing