Theorems · Definition · field theory

Field.casesOn

{K : Type u} →
  {motive : Field K → Sort u_1} →
    (t : Field K) →
      ([toCommRing : CommRing 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
                                                { toCommRing := toCommRing, 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