Theorems · Definition · field theory

Function.Injective.divisionSemiring

{K : Type u_1} →
  {L : Type u_2} →
    [inst : Zero K] →
      [inst_1 : Add K] →
        [inst_2 : One K] →
          [inst_3 : Mul K] →
            [inst_4 : Inv K] →
              [inst_5 : Div K] →
                [inst_6 : SMul ℕ K] →
                  [inst_7 : SMul ℚ≥0 K] →
                    [inst_8 : Pow K ℕ] →
                      [inst_9 : Pow K ℤ] →
                        [inst_10 : NatCast K] →
                          [inst_11 : NNRatCast K] →
                            (f : K → L) →
                              Function.Injective f →
                                [inst_12 : DivisionSemiring 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) →
                                              (∀ (n : ℕ) (x : K), f (n • x) = n • f x) →
                                                (∀ (q : ℚ≥0) (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) →
                                                        (∀ (q : ℚ≥0), f ↑q = ↑q) → DivisionSemiring K

Pullback a DivisionSemiring along an injective function.

Defined in

Mathlib.Algebra.Field.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

ZeroAddOneMulInvDivSMulSMulPowPowNatCastNNRatCastDivisionSemiring