Theorems · Definition · functional analysis

RCLike.recOn

{K : Type u_1} →
  {motive : RCLike K → Sort u} →
    (t : RCLike K) →
      ([toDenselyNormedField : DenselyNormedField K] →
          [toStarRing : StarRing K] →
            [toNormedAlgebra : NormedAlgebra ℝ K] →
              [toCompleteSpace : CompleteSpace K] →
                (re im : K →+ ℝ) →
                  (I : K) →
                    (I_re_ax : re I = 0) →
                      (I_mul_I_ax : I = 0 ∨ I * I = -1) →
                        (re_add_im_ax : ∀ (z : K), (algebraMap ℝ K) (re z) + (algebraMap ℝ K) (im z) * I = z) →
                          (ofReal_re_ax : ∀ (r : ℝ), re ((algebraMap ℝ K) r) = r) →
                            (ofReal_im_ax : ∀ (r : ℝ), im ((algebraMap ℝ K) r) = 0) →
                              (mul_re_ax : ∀ (z w : K), re (z * w) = re z * re w - im z * im w) →
                                (mul_im_ax : ∀ (z w : K), im (z * w) = re z * im w + im z * re w) →
                                  (conj_re_ax : ∀ (z : K), re ((starRingEnd K) z) = re z) →
                                    (conj_im_ax : ∀ (z : K), im ((starRingEnd K) z) = -im z) →
                                      (conj_I_ax : (starRingEnd K) I = -I) →
                                        (norm_sq_eq_def_ax : ∀ (z : K), ‖z‖ ^ 2 = re z * re z + im z * im z) →
                                          (mul_im_I_ax : ∀ (z : K), im z * im I = im z) →
                                            [toPartialOrder : PartialOrder K] →
                                              (le_iff_re_im : ∀ {z w : K}, z ≤ w ↔ re z ≤ re w ∧ im z = im w) →
                                                [toDecidableEq : DecidableEq K] →
                                                  motive
                                                    { toDenselyNormedField := toDenselyNormedField,
                                                      toStarRing := toStarRing, toNormedAlgebra := toNormedAlgebra,
                                                      toCompleteSpace := toCompleteSpace, re := re, im := im, I := I,
                                                      I_re_ax := I_re_ax, I_mul_I_ax := I_mul_I_ax,
                                                      re_add_im_ax := re_add_im_ax, ofReal_re_ax := ofReal_re_ax,
                                                      ofReal_im_ax := ofReal_im_ax, mul_re_ax := mul_re_ax,
                                                      mul_im_ax := mul_im_ax, conj_re_ax := conj_re_ax,
                                                      conj_im_ax := conj_im_ax, conj_I_ax := conj_I_ax,
                                                      norm_sq_eq_def_ax := norm_sq_eq_def_ax,
                                                      mul_im_I_ax := mul_im_I_ax, toPartialOrder := toPartialOrder,
                                                      le_iff_re_im := le_iff_re_im, toDecidableEq := toDecidableEq }) →
        motive t

Defined in

Mathlib.Analysis.RCLike.Basic

Cited by

0 results in Mathlib

Foundations

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