Theorems · Definition · field theory

DivisionRing.recOn

{K : Type u_2} →
  {motive : DivisionRing K → Sort u} →
    (t : DivisionRing K) →
      ([toRing : Ring K] →
          [toInv : Inv K] →
            [toDiv : Div K] →
              [toZPow : ZPow K] →
                (div_eq_mul_inv : ∀ (a b : K), a / b = a * b⁻¹) →
                  (zpow_zero' : ∀ (a : K), a ^ 0 = 1) →
                    (zpow_succ' : ∀ (n : ℕ) (a : K), a ^ ↑n.succ = a ^ ↑n * a) →
                      (zpow_neg' : ∀ (n : ℕ) (a : K), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹) →
                        [toNontrivial : Nontrivial K] →
                          [toNNRatCast : NNRatCast K] →
                            [toRatCast : RatCast K] →
                              (mul_inv_cancel : ∀ (a : K), a ≠ 0 → a * a⁻¹ = 1) →
                                (inv_zero : 0⁻¹ = 0) →
                                  (nnratCast_def : ∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den) →
                                    (nnqsmul : ℚ≥0 → K → K) →
                                      (nnqsmul_def : ∀ (q : ℚ≥0) (a : K), nnqsmul q a = ↑q * a) →
                                        (ratCast_def : ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den) →
                                          (qsmul : ℚ → K → K) →
                                            (qsmul_def : ∀ (a : ℚ) (x : K), qsmul a x = ↑a * x) →
                                              motive
                                                { toRing := toRing, toInv := toInv, toDiv := toDiv, toZPow := toZPow,
                                                  div_eq_mul_inv := div_eq_mul_inv, zpow_zero' := zpow_zero',
                                                  zpow_succ' := zpow_succ', zpow_neg' := zpow_neg',
                                                  toNontrivial := toNontrivial, toNNRatCast := toNNRatCast,
                                                  toRatCast := toRatCast, mul_inv_cancel := mul_inv_cancel,
                                                  inv_zero := inv_zero, nnratCast_def := nnratCast_def,
                                                  nnqsmul := nnqsmul, nnqsmul_def := nnqsmul_def,
                                                  ratCast_def := ratCast_def, qsmul := qsmul,
                                                  qsmul_def := qsmul_def }) →
        motive t

Defined in

Mathlib.Algebra.Field.Defs

Cited by

0 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound