Documentation

Mathlib.Algebra.Quaternion

Quaternions #

In this file we define quaternions ℍ[R] over a commutative ring R, and define some algebraic structures on ℍ[R].

Main definitions #

We also define the following algebraic structures on ℍ[R]:

Notation #

The following notation is available with open Quaternion or open scoped Quaternion.

Implementation notes #

We define quaternions over any ring R, not just to be able to deal with, e.g., integer or rational quaternions without using real numbers. In particular, all definitions in this file are computable.

Tags #

quaternion

theorem QuaternionAlgebra.ext {R : Type u_1} {a : R} {b : R} (x : QuaternionAlgebra R a b) (y : QuaternionAlgebra R a b) (re : x.re = y.re) (imI : x.imI = y.imI) (imJ : x.imJ = y.imJ) (imK : x.imK = y.imK) :
x = y
theorem QuaternionAlgebra.ext_iff {R : Type u_1} {a : R} {b : R} (x : QuaternionAlgebra R a b) (y : QuaternionAlgebra R a b) :
x = y x.re = y.re x.imI = y.imI x.imJ = y.imJ x.imK = y.imK
structure QuaternionAlgebra (R : Type u_1) (a : R) (b : R) :
Type u_1

Quaternion algebra over a type with fixed coefficients $a=i^2$ and $b=j^2$. Implemented as a structure with four fields: re, imI, imJ, and imK.

  • re : R

    Real part of a quaternion.

  • imI : R
  • imJ : R
  • imK : R
Instances For

    Quaternion algebra over a type with fixed coefficients $a=i^2$ and $b=j^2$. Implemented as a structure with four fields: re, imI, imJ, and imK.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem QuaternionAlgebra.equivProd_apply {R : Type u_1} (c₁ : R) (c₂ : R) (a : QuaternionAlgebra R c₁ c₂) :
      (QuaternionAlgebra.equivProd c₁ c₂) a = (a.re, a.imI, a.imJ, a.imK)
      @[simp]
      theorem QuaternionAlgebra.equivProd_symm_apply_imK {R : Type u_1} (c₁ : R) (c₂ : R) (a : R × R × R × R) :
      ((QuaternionAlgebra.equivProd c₁ c₂).symm a).imK = a.2.2.2
      @[simp]
      theorem QuaternionAlgebra.equivProd_symm_apply_re {R : Type u_1} (c₁ : R) (c₂ : R) (a : R × R × R × R) :
      ((QuaternionAlgebra.equivProd c₁ c₂).symm a).re = a.1
      @[simp]
      theorem QuaternionAlgebra.equivProd_symm_apply_imJ {R : Type u_1} (c₁ : R) (c₂ : R) (a : R × R × R × R) :
      ((QuaternionAlgebra.equivProd c₁ c₂).symm a).imJ = a.2.2.1
      @[simp]
      theorem QuaternionAlgebra.equivProd_symm_apply_imI {R : Type u_1} (c₁ : R) (c₂ : R) (a : R × R × R × R) :
      ((QuaternionAlgebra.equivProd c₁ c₂).symm a).imI = a.2.1
      def QuaternionAlgebra.equivProd {R : Type u_1} (c₁ : R) (c₂ : R) :
      QuaternionAlgebra R c₁ c₂ R × R × R × R

      The equivalence between a quaternion algebra over R and R × R × R × R.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem QuaternionAlgebra.equivTuple_symm_apply {R : Type u_1} (c₁ : R) (c₂ : R) (a : Fin 4R) :
        (QuaternionAlgebra.equivTuple c₁ c₂).symm a = { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }
        def QuaternionAlgebra.equivTuple {R : Type u_1} (c₁ : R) (c₂ : R) :
        QuaternionAlgebra R c₁ c₂ (Fin 4R)

        The equivalence between a quaternion algebra over R and Fin 4 → R.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem QuaternionAlgebra.equivTuple_apply {R : Type u_1} (c₁ : R) (c₂ : R) (x : QuaternionAlgebra R c₁ c₂) :
          (QuaternionAlgebra.equivTuple c₁ c₂) x = ![x.re, x.imI, x.imJ, x.imK]
          @[simp]
          theorem QuaternionAlgebra.mk.eta {R : Type u_1} {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
          { re := a.re, imI := a.imI, imJ := a.imJ, imK := a.imK } = a
          instance QuaternionAlgebra.instSubsingleton {R : Type u_3} {c₁ : R} {c₂ : R} [Subsingleton R] :
          Equations
          • =
          instance QuaternionAlgebra.instNontrivial {R : Type u_3} {c₁ : R} {c₂ : R} [Nontrivial R] :
          Equations
          • =
          def QuaternionAlgebra.im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (x : QuaternionAlgebra R c₁ c₂) :
          QuaternionAlgebra R c₁ c₂

          The imaginary part of a quaternion.

          Equations
          • x.im = { re := 0, imI := x.imI, imJ := x.imJ, imK := x.imK }
          Instances For
            @[simp]
            theorem QuaternionAlgebra.im_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
            a.im.re = 0
            @[simp]
            theorem QuaternionAlgebra.im_imI {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
            a.im.imI = a.imI
            @[simp]
            theorem QuaternionAlgebra.im_imJ {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
            a.im.imJ = a.imJ
            @[simp]
            theorem QuaternionAlgebra.im_imK {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
            a.im.imK = a.imK
            @[simp]
            theorem QuaternionAlgebra.im_idem {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
            a.im.im = a.im
            def QuaternionAlgebra.coe {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (x : R) :
            QuaternionAlgebra R c₁ c₂

            Coercion R → ℍ[R,c₁,c₂].

            Equations
            • x = { re := x, imI := 0, imJ := 0, imK := 0 }
            Instances For
              instance QuaternionAlgebra.instCoeTC {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              CoeTC R (QuaternionAlgebra R c₁ c₂)
              Equations
              • QuaternionAlgebra.instCoeTC = { coe := QuaternionAlgebra.coe }
              @[simp]
              theorem QuaternionAlgebra.coe_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (x : R) :
              (x).re = x
              @[simp]
              theorem QuaternionAlgebra.coe_imI {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (x : R) :
              (x).imI = 0
              @[simp]
              theorem QuaternionAlgebra.coe_imJ {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (x : R) :
              (x).imJ = 0
              @[simp]
              theorem QuaternionAlgebra.coe_imK {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (x : R) :
              (x).imK = 0
              theorem QuaternionAlgebra.coe_injective {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              Function.Injective QuaternionAlgebra.coe
              @[simp]
              theorem QuaternionAlgebra.coe_inj {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} {x : R} {y : R} :
              x = y x = y
              instance QuaternionAlgebra.instZero {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              Zero (QuaternionAlgebra R c₁ c₂)
              Equations
              • QuaternionAlgebra.instZero = { zero := { re := 0, imI := 0, imJ := 0, imK := 0 } }
              @[simp]
              theorem QuaternionAlgebra.zero_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              @[simp]
              theorem QuaternionAlgebra.zero_imI {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              @[simp]
              theorem QuaternionAlgebra.zero_imJ {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              @[simp]
              theorem QuaternionAlgebra.zero_imK {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              @[simp]
              theorem QuaternionAlgebra.zero_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              @[simp]
              theorem QuaternionAlgebra.coe_zero {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              0 = 0
              instance QuaternionAlgebra.instInhabited {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              Equations
              • QuaternionAlgebra.instInhabited = { default := 0 }
              instance QuaternionAlgebra.instOne {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              One (QuaternionAlgebra R c₁ c₂)
              Equations
              • QuaternionAlgebra.instOne = { one := { re := 1, imI := 0, imJ := 0, imK := 0 } }
              @[simp]
              theorem QuaternionAlgebra.one_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              @[simp]
              theorem QuaternionAlgebra.one_imI {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              @[simp]
              theorem QuaternionAlgebra.one_imJ {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              @[simp]
              theorem QuaternionAlgebra.one_imK {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              @[simp]
              theorem QuaternionAlgebra.one_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              @[simp]
              theorem QuaternionAlgebra.coe_one {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              1 = 1
              instance QuaternionAlgebra.instAdd {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              Add (QuaternionAlgebra R c₁ c₂)
              Equations
              • QuaternionAlgebra.instAdd = { add := fun (a b : QuaternionAlgebra R c₁ c₂) => { re := a.re + b.re, imI := a.imI + b.imI, imJ := a.imJ + b.imJ, imK := a.imK + b.imK } }
              @[simp]
              theorem QuaternionAlgebra.add_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) (b : QuaternionAlgebra R c₁ c₂) :
              (a + b).re = a.re + b.re
              @[simp]
              theorem QuaternionAlgebra.add_imI {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) (b : QuaternionAlgebra R c₁ c₂) :
              (a + b).imI = a.imI + b.imI
              @[simp]
              theorem QuaternionAlgebra.add_imJ {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) (b : QuaternionAlgebra R c₁ c₂) :
              (a + b).imJ = a.imJ + b.imJ
              @[simp]
              theorem QuaternionAlgebra.add_imK {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) (b : QuaternionAlgebra R c₁ c₂) :
              (a + b).imK = a.imK + b.imK
              @[simp]
              theorem QuaternionAlgebra.add_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) (b : QuaternionAlgebra R c₁ c₂) :
              (a + b).im = a.im + b.im
              @[simp]
              theorem QuaternionAlgebra.mk_add_mk {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a₁ : R) (a₂ : R) (a₃ : R) (a₄ : R) (b₁ : R) (b₂ : R) (b₃ : R) (b₄ : R) :
              { re := a₁, imI := a₂, imJ := a₃, imK := a₄ } + { re := b₁, imI := b₂, imJ := b₃, imK := b₄ } = { re := a₁ + b₁, imI := a₂ + b₂, imJ := a₃ + b₃, imK := a₄ + b₄ }
              @[simp]
              theorem QuaternionAlgebra.coe_add {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (x : R) (y : R) :
              (x + y) = x + y
              instance QuaternionAlgebra.instNeg {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              Neg (QuaternionAlgebra R c₁ c₂)
              Equations
              • QuaternionAlgebra.instNeg = { neg := fun (a : QuaternionAlgebra R c₁ c₂) => { re := -a.re, imI := -a.imI, imJ := -a.imJ, imK := -a.imK } }
              @[simp]
              theorem QuaternionAlgebra.neg_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
              (-a).re = -a.re
              @[simp]
              theorem QuaternionAlgebra.neg_imI {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
              (-a).imI = -a.imI
              @[simp]
              theorem QuaternionAlgebra.neg_imJ {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
              (-a).imJ = -a.imJ
              @[simp]
              theorem QuaternionAlgebra.neg_imK {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
              (-a).imK = -a.imK
              @[simp]
              theorem QuaternionAlgebra.neg_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
              (-a).im = -a.im
              @[simp]
              theorem QuaternionAlgebra.neg_mk {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a₁ : R) (a₂ : R) (a₃ : R) (a₄ : R) :
              -{ re := a₁, imI := a₂, imJ := a₃, imK := a₄ } = { re := -a₁, imI := -a₂, imJ := -a₃, imK := -a₄ }
              @[simp]
              theorem QuaternionAlgebra.coe_neg {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (x : R) :
              (-x) = -x
              instance QuaternionAlgebra.instSub {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              Sub (QuaternionAlgebra R c₁ c₂)
              Equations
              • QuaternionAlgebra.instSub = { sub := fun (a b : QuaternionAlgebra R c₁ c₂) => { re := a.re - b.re, imI := a.imI - b.imI, imJ := a.imJ - b.imJ, imK := a.imK - b.imK } }
              @[simp]
              theorem QuaternionAlgebra.sub_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) (b : QuaternionAlgebra R c₁ c₂) :
              (a - b).re = a.re - b.re
              @[simp]
              theorem QuaternionAlgebra.sub_imI {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) (b : QuaternionAlgebra R c₁ c₂) :
              (a - b).imI = a.imI - b.imI
              @[simp]
              theorem QuaternionAlgebra.sub_imJ {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) (b : QuaternionAlgebra R c₁ c₂) :
              (a - b).imJ = a.imJ - b.imJ
              @[simp]
              theorem QuaternionAlgebra.sub_imK {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) (b : QuaternionAlgebra R c₁ c₂) :
              (a - b).imK = a.imK - b.imK
              @[simp]
              theorem QuaternionAlgebra.sub_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) (b : QuaternionAlgebra R c₁ c₂) :
              (a - b).im = a.im - b.im
              @[simp]
              theorem QuaternionAlgebra.mk_sub_mk {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a₁ : R) (a₂ : R) (a₃ : R) (a₄ : R) (b₁ : R) (b₂ : R) (b₃ : R) (b₄ : R) :
              { re := a₁, imI := a₂, imJ := a₃, imK := a₄ } - { re := b₁, imI := b₂, imJ := b₃, imK := b₄ } = { re := a₁ - b₁, imI := a₂ - b₂, imJ := a₃ - b₃, imK := a₄ - b₄ }
              @[simp]
              theorem QuaternionAlgebra.coe_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (x : R) :
              (x).im = 0
              @[simp]
              theorem QuaternionAlgebra.re_add_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
              a.re + a.im = a
              @[simp]
              theorem QuaternionAlgebra.sub_self_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
              a - a.im = a.re
              @[simp]
              theorem QuaternionAlgebra.sub_self_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
              a - a.re = a.im
              instance QuaternionAlgebra.instMul {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              Mul (QuaternionAlgebra R c₁ c₂)

              Multiplication is given by

              • 1 * x = x * 1 = x;
              • i * i = c₁;
              • j * j = c₂;
              • i * j = k, j * i = -k;
              • k * k = -c₁ * c₂;
              • i * k = c₁ * j, k * i = -c₁ * j;
              • j * k = -c₂ * i, k * j = c₂ * i.
              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem QuaternionAlgebra.mul_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) (b : QuaternionAlgebra R c₁ c₂) :
              (a * b).re = a.re * b.re + c₁ * a.imI * b.imI + c₂ * a.imJ * b.imJ - c₁ * c₂ * a.imK * b.imK
              @[simp]
              theorem QuaternionAlgebra.mul_imI {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) (b : QuaternionAlgebra R c₁ c₂) :
              (a * b).imI = a.re * b.imI + a.imI * b.re - c₂ * a.imJ * b.imK + c₂ * a.imK * b.imJ
              @[simp]
              theorem QuaternionAlgebra.mul_imJ {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) (b : QuaternionAlgebra R c₁ c₂) :
              (a * b).imJ = a.re * b.imJ + c₁ * a.imI * b.imK + a.imJ * b.re - c₁ * a.imK * b.imI
              @[simp]
              theorem QuaternionAlgebra.mul_imK {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) (b : QuaternionAlgebra R c₁ c₂) :
              (a * b).imK = a.re * b.imK + a.imI * b.imJ - a.imJ * b.imI + a.imK * b.re
              @[simp]
              theorem QuaternionAlgebra.mk_mul_mk {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a₁ : R) (a₂ : R) (a₃ : R) (a₄ : R) (b₁ : R) (b₂ : R) (b₃ : R) (b₄ : R) :
              { re := a₁, imI := a₂, imJ := a₃, imK := a₄ } * { re := b₁, imI := b₂, imJ := b₃, imK := b₄ } = { re := a₁ * b₁ + c₁ * a₂ * b₂ + c₂ * a₃ * b₃ - c₁ * c₂ * a₄ * b₄, imI := a₁ * b₂ + a₂ * b₁ - c₂ * a₃ * b₄ + c₂ * a₄ * b₃, imJ := a₁ * b₃ + c₁ * a₂ * b₄ + a₃ * b₁ - c₁ * a₄ * b₂, imK := a₁ * b₄ + a₂ * b₃ - a₃ * b₂ + a₄ * b₁ }
              instance QuaternionAlgebra.instSMul {S : Type u_1} {R : Type u_3} {c₁ : R} {c₂ : R} [SMul S R] :
              SMul S (QuaternionAlgebra R c₁ c₂)
              Equations
              • QuaternionAlgebra.instSMul = { smul := fun (s : S) (a : QuaternionAlgebra R c₁ c₂) => { re := s a.re, imI := s a.imI, imJ := s a.imJ, imK := s a.imK } }
              instance QuaternionAlgebra.instIsScalarTower {S : Type u_1} {T : Type u_2} {R : Type u_3} {c₁ : R} {c₂ : R} [SMul S R] [SMul T R] [SMul S T] [IsScalarTower S T R] :
              Equations
              • =
              instance QuaternionAlgebra.instSMulCommClass {S : Type u_1} {T : Type u_2} {R : Type u_3} {c₁ : R} {c₂ : R} [SMul S R] [SMul T R] [SMulCommClass S T R] :
              Equations
              • =
              @[simp]
              theorem QuaternionAlgebra.smul_re {S : Type u_1} {R : Type u_3} {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) [SMul S R] (s : S) :
              (s a).re = s a.re
              @[simp]
              theorem QuaternionAlgebra.smul_imI {S : Type u_1} {R : Type u_3} {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) [SMul S R] (s : S) :
              (s a).imI = s a.imI
              @[simp]
              theorem QuaternionAlgebra.smul_imJ {S : Type u_1} {R : Type u_3} {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) [SMul S R] (s : S) :
              (s a).imJ = s a.imJ
              @[simp]
              theorem QuaternionAlgebra.smul_imK {S : Type u_1} {R : Type u_3} {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) [SMul S R] (s : S) :
              (s a).imK = s a.imK
              @[simp]
              theorem QuaternionAlgebra.smul_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) {S : Type u_4} [SMulZeroClass S R] (s : S) :
              (s a).im = s a.im
              @[simp]
              theorem QuaternionAlgebra.smul_mk {S : Type u_1} {R : Type u_3} {c₁ : R} {c₂ : R} [SMul S R] (s : S) (re : R) (im_i : R) (im_j : R) (im_k : R) :
              s { re := re, imI := im_i, imJ := im_j, imK := im_k } = { re := s re, imI := s im_i, imJ := s im_j, imK := s im_k }
              @[simp]
              theorem QuaternionAlgebra.coe_smul {S : Type u_1} {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} [SMulZeroClass S R] (s : S) (r : R) :
              (s r) = s r
              instance QuaternionAlgebra.instAddCommGroup {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              Equations
              instance QuaternionAlgebra.instAddCommGroupWithOne {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              Equations
              @[simp]
              theorem QuaternionAlgebra.natCast_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (n : ) :
              (n).re = n
              @[simp]
              theorem QuaternionAlgebra.natCast_imI {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (n : ) :
              (n).imI = 0
              @[simp]
              theorem QuaternionAlgebra.natCast_imJ {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (n : ) :
              (n).imJ = 0
              @[simp]
              theorem QuaternionAlgebra.natCast_imK {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (n : ) :
              (n).imK = 0
              @[simp]
              theorem QuaternionAlgebra.natCast_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (n : ) :
              (n).im = 0
              theorem QuaternionAlgebra.coe_natCast {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (n : ) :
              n = n
              @[simp]
              theorem QuaternionAlgebra.intCast_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (z : ) :
              (z).re = z
              @[simp]
              theorem QuaternionAlgebra.intCast_imI {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (z : ) :
              (z).imI = 0
              @[simp]
              theorem QuaternionAlgebra.intCast_imJ {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (z : ) :
              (z).imJ = 0
              @[simp]
              theorem QuaternionAlgebra.intCast_imK {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (z : ) :
              (z).imK = 0
              @[simp]
              theorem QuaternionAlgebra.intCast_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (z : ) :
              (z).im = 0
              theorem QuaternionAlgebra.coe_intCast {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (z : ) :
              z = z
              instance QuaternionAlgebra.instRing {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              Ring (QuaternionAlgebra R c₁ c₂)
              Equations
              @[simp]
              theorem QuaternionAlgebra.coe_mul {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (x : R) (y : R) :
              (x * y) = x * y
              instance QuaternionAlgebra.instAlgebra {S : Type u_1} {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} [CommSemiring S] [Algebra S R] :
              Algebra S (QuaternionAlgebra R c₁ c₂)
              Equations
              • QuaternionAlgebra.instAlgebra = Algebra.mk { toFun := fun (s : S) => ((algebraMap S R) s), map_one' := , map_mul' := , map_zero' := , map_add' := }
              theorem QuaternionAlgebra.algebraMap_eq {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (r : R) :
              (algebraMap R (QuaternionAlgebra R c₁ c₂)) r = { re := r, imI := 0, imJ := 0, imK := 0 }
              theorem QuaternionAlgebra.algebraMap_injective {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              Equations
              • =
              @[simp]
              theorem QuaternionAlgebra.reₗ_apply {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) (self : QuaternionAlgebra R c₁ c₂) :
              (QuaternionAlgebra.reₗ c₁ c₂) self = self.re
              def QuaternionAlgebra.reₗ {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) :

              QuaternionAlgebra.re as a LinearMap

              Equations
              Instances For
                @[simp]
                theorem QuaternionAlgebra.imIₗ_apply {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) (self : QuaternionAlgebra R c₁ c₂) :
                (QuaternionAlgebra.imIₗ c₁ c₂) self = self.imI
                def QuaternionAlgebra.imIₗ {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) :

                QuaternionAlgebra.imI as a LinearMap

                Equations
                Instances For
                  @[simp]
                  theorem QuaternionAlgebra.imJₗ_apply {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) (self : QuaternionAlgebra R c₁ c₂) :
                  (QuaternionAlgebra.imJₗ c₁ c₂) self = self.imJ
                  def QuaternionAlgebra.imJₗ {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) :

                  QuaternionAlgebra.imJ as a LinearMap

                  Equations
                  Instances For
                    @[simp]
                    theorem QuaternionAlgebra.imKₗ_apply {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) (self : QuaternionAlgebra R c₁ c₂) :
                    (QuaternionAlgebra.imKₗ c₁ c₂) self = self.imK
                    def QuaternionAlgebra.imKₗ {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) :

                    QuaternionAlgebra.imK as a LinearMap

                    Equations
                    Instances For
                      def QuaternionAlgebra.linearEquivTuple {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) :
                      QuaternionAlgebra R c₁ c₂ ≃ₗ[R] Fin 4R

                      QuaternionAlgebra.equivTuple as a linear equivalence.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem QuaternionAlgebra.coe_linearEquivTuple {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) :
                        @[simp]
                        theorem QuaternionAlgebra.coe_linearEquivTuple_symm {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) :
                        (QuaternionAlgebra.linearEquivTuple c₁ c₂).symm = (QuaternionAlgebra.equivTuple c₁ c₂).symm
                        noncomputable def QuaternionAlgebra.basisOneIJK {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) :
                        Basis (Fin 4) R (QuaternionAlgebra R c₁ c₂)

                        ℍ[R, c₁, c₂] has a basis over R given by 1, i, j, and k.

                        Equations
                        Instances For
                          @[simp]
                          theorem QuaternionAlgebra.coe_basisOneIJK_repr {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) (q : QuaternionAlgebra R c₁ c₂) :
                          ((QuaternionAlgebra.basisOneIJK c₁ c₂).repr q) = ![q.re, q.imI, q.imJ, q.imK]
                          instance QuaternionAlgebra.instFinite {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) :
                          Equations
                          • =
                          instance QuaternionAlgebra.instFree {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) :
                          Equations
                          • =
                          theorem QuaternionAlgebra.rank_eq_four {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) [StrongRankCondition R] :
                          Module.rank R (QuaternionAlgebra R c₁ c₂) = 4
                          @[simp]
                          theorem QuaternionAlgebra.swapEquiv_symm_apply_imI {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) (t : QuaternionAlgebra R c₂ c₁) :
                          ((QuaternionAlgebra.swapEquiv c₁ c₂).symm t).imI = t.imJ
                          @[simp]
                          theorem QuaternionAlgebra.swapEquiv_apply_imI {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) (t : QuaternionAlgebra R c₁ c₂) :
                          ((QuaternionAlgebra.swapEquiv c₁ c₂) t).imI = t.imJ
                          @[simp]
                          theorem QuaternionAlgebra.swapEquiv_apply_imK {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) (t : QuaternionAlgebra R c₁ c₂) :
                          ((QuaternionAlgebra.swapEquiv c₁ c₂) t).imK = -t.imK
                          @[simp]
                          theorem QuaternionAlgebra.swapEquiv_symm_apply_re {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) (t : QuaternionAlgebra R c₂ c₁) :
                          ((QuaternionAlgebra.swapEquiv c₁ c₂).symm t).re = t.re
                          @[simp]
                          theorem QuaternionAlgebra.swapEquiv_apply_re {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) (t : QuaternionAlgebra R c₁ c₂) :
                          ((QuaternionAlgebra.swapEquiv c₁ c₂) t).re = t.re
                          @[simp]
                          theorem QuaternionAlgebra.swapEquiv_symm_apply_imJ {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) (t : QuaternionAlgebra R c₂ c₁) :
                          ((QuaternionAlgebra.swapEquiv c₁ c₂).symm t).imJ = t.imI
                          @[simp]
                          theorem QuaternionAlgebra.swapEquiv_symm_apply_imK {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) (t : QuaternionAlgebra R c₂ c₁) :
                          ((QuaternionAlgebra.swapEquiv c₁ c₂).symm t).imK = -t.imK
                          @[simp]
                          theorem QuaternionAlgebra.swapEquiv_apply_imJ {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) (t : QuaternionAlgebra R c₁ c₂) :
                          ((QuaternionAlgebra.swapEquiv c₁ c₂) t).imJ = t.imI
                          def QuaternionAlgebra.swapEquiv {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) :

                          There is a natural equivalence when swapping the coefficients of a quaternion algebra.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem QuaternionAlgebra.coe_sub {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (x : R) (y : R) :
                            (x - y) = x - y
                            @[simp]
                            theorem QuaternionAlgebra.coe_pow {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (x : R) (n : ) :
                            (x ^ n) = x ^ n
                            theorem QuaternionAlgebra.coe_commutes {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (r : R) (a : QuaternionAlgebra R c₁ c₂) :
                            r * a = a * r
                            theorem QuaternionAlgebra.coe_commute {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (r : R) (a : QuaternionAlgebra R c₁ c₂) :
                            Commute (r) a
                            theorem QuaternionAlgebra.coe_mul_eq_smul {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (r : R) (a : QuaternionAlgebra R c₁ c₂) :
                            r * a = r a
                            theorem QuaternionAlgebra.mul_coe_eq_smul {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (r : R) (a : QuaternionAlgebra R c₁ c₂) :
                            a * r = r a
                            @[simp]
                            theorem QuaternionAlgebra.coe_algebraMap {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
                            (algebraMap R (QuaternionAlgebra R c₁ c₂)) = QuaternionAlgebra.coe
                            theorem QuaternionAlgebra.smul_coe {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (x : R) (y : R) :
                            x y = (x * y)
                            instance QuaternionAlgebra.instStarQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
                            Star (QuaternionAlgebra R c₁ c₂)

                            Quaternion conjugate.

                            Equations
                            • QuaternionAlgebra.instStarQuaternionAlgebra = { star := fun (a : QuaternionAlgebra R c₁ c₂) => { re := a.re, imI := -a.imI, imJ := -a.imJ, imK := -a.imK } }
                            @[simp]
                            theorem QuaternionAlgebra.re_star {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
                            (star a).re = a.re
                            @[simp]
                            theorem QuaternionAlgebra.imI_star {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
                            (star a).imI = -a.imI
                            @[simp]
                            theorem QuaternionAlgebra.imJ_star {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
                            (star a).imJ = -a.imJ
                            @[simp]
                            theorem QuaternionAlgebra.imK_star {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
                            (star a).imK = -a.imK
                            @[simp]
                            theorem QuaternionAlgebra.im_star {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
                            (star a).im = -a.im
                            @[simp]
                            theorem QuaternionAlgebra.star_mk {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a₁ : R) (a₂ : R) (a₃ : R) (a₄ : R) :
                            star { re := a₁, imI := a₂, imJ := a₃, imK := a₄ } = { re := a₁, imI := -a₂, imJ := -a₃, imK := -a₄ }
                            instance QuaternionAlgebra.instStarRing {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
                            Equations
                            theorem QuaternionAlgebra.self_add_star' {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
                            a + star a = (2 * a.re)
                            theorem QuaternionAlgebra.self_add_star {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
                            a + star a = 2 * a.re
                            theorem QuaternionAlgebra.star_add_self' {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
                            star a + a = (2 * a.re)
                            theorem QuaternionAlgebra.star_add_self {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
                            star a + a = 2 * a.re
                            theorem QuaternionAlgebra.star_eq_two_re_sub {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
                            star a = (2 * a.re) - a
                            instance QuaternionAlgebra.instIsStarNormal {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
                            Equations
                            • =
                            @[simp]
                            theorem QuaternionAlgebra.star_coe {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (x : R) :
                            star x = x
                            @[simp]
                            theorem QuaternionAlgebra.star_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
                            star a.im = -a.im
                            @[simp]
                            theorem QuaternionAlgebra.star_smul {S : Type u_1} {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} [Monoid S] [DistribMulAction S R] (s : S) (a : QuaternionAlgebra R c₁ c₂) :
                            star (s a) = s star a
                            theorem QuaternionAlgebra.eq_re_of_eq_coe {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} {a : QuaternionAlgebra R c₁ c₂} {x : R} (h : a = x) :
                            a = a.re
                            theorem QuaternionAlgebra.eq_re_iff_mem_range_coe {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} {a : QuaternionAlgebra R c₁ c₂} :
                            a = a.re a Set.range QuaternionAlgebra.coe
                            @[simp]
                            theorem QuaternionAlgebra.star_eq_self {R : Type u_3} [CommRing R] [NoZeroDivisors R] [CharZero R] {c₁ : R} {c₂ : R} {a : QuaternionAlgebra R c₁ c₂} :
                            star a = a a = a.re
                            theorem QuaternionAlgebra.star_eq_neg {R : Type u_3} [CommRing R] [NoZeroDivisors R] [CharZero R] {c₁ : R} {c₂ : R} {a : QuaternionAlgebra R c₁ c₂} :
                            star a = -a a.re = 0
                            theorem QuaternionAlgebra.star_mul_eq_coe {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
                            star a * a = (star a * a).re
                            theorem QuaternionAlgebra.mul_star_eq_coe {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
                            a * star a = (a * star a).re
                            def QuaternionAlgebra.starAe {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :

                            Quaternion conjugate as an AlgEquiv to the opposite ring.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[simp]
                              theorem QuaternionAlgebra.coe_starAe {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
                              QuaternionAlgebra.starAe = MulOpposite.op star
                              def Quaternion (R : Type u_1) [One R] [Neg R] :
                              Type u_1

                              Space of quaternions over a type. Implemented as a structure with four fields: re, im_i, im_j, and im_k.

                              Equations
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[simp]
                                  theorem Quaternion.equivProd_symm_apply_imI (R : Type u_1) [One R] [Neg R] (a : R × R × R × R) :
                                  ((Quaternion.equivProd R).symm a).imI = a.2.1
                                  @[simp]
                                  theorem Quaternion.equivProd_apply (R : Type u_1) [One R] [Neg R] (a : QuaternionAlgebra R (-1) (-1)) :
                                  (Quaternion.equivProd R) a = (a.re, a.imI, a.imJ, a.imK)
                                  @[simp]
                                  theorem Quaternion.equivProd_symm_apply_re (R : Type u_1) [One R] [Neg R] (a : R × R × R × R) :
                                  ((Quaternion.equivProd R).symm a).re = a.1
                                  @[simp]
                                  theorem Quaternion.equivProd_symm_apply_imK (R : Type u_1) [One R] [Neg R] (a : R × R × R × R) :
                                  ((Quaternion.equivProd R).symm a).imK = a.2.2.2
                                  @[simp]
                                  theorem Quaternion.equivProd_symm_apply_imJ (R : Type u_1) [One R] [Neg R] (a : R × R × R × R) :
                                  ((Quaternion.equivProd R).symm a).imJ = a.2.2.1
                                  def Quaternion.equivProd (R : Type u_1) [One R] [Neg R] :
                                  Quaternion R R × R × R × R

                                  The equivalence between the quaternions over R and R × R × R × R.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem Quaternion.equivTuple_symm_apply (R : Type u_1) [One R] [Neg R] (a : Fin 4R) :
                                    (Quaternion.equivTuple R).symm a = { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }
                                    def Quaternion.equivTuple (R : Type u_1) [One R] [Neg R] :
                                    Quaternion R (Fin 4R)

                                    The equivalence between the quaternions over R and Fin 4 → R.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem Quaternion.equivTuple_apply (R : Type u_1) [One R] [Neg R] (x : Quaternion R) :
                                      (Quaternion.equivTuple R) x = ![x.re, x.imI, x.imJ, x.imK]
                                      Equations
                                      • =
                                      Equations
                                      • =
                                      def Quaternion.coe {R : Type u_3} [CommRing R] :
                                      RQuaternion R

                                      Coercion R → ℍ[R].

                                      Equations
                                      • Quaternion.coe = QuaternionAlgebra.coe
                                      Instances For
                                        instance Quaternion.instCoeTC {R : Type u_3} [CommRing R] :
                                        Equations
                                        • Quaternion.instCoeTC = { coe := Quaternion.coe }
                                        instance Quaternion.instRing {R : Type u_3} [CommRing R] :
                                        Equations
                                        • Quaternion.instRing = QuaternionAlgebra.instRing
                                        Equations
                                        instance Quaternion.instSMul {S : Type u_1} {R : Type u_3} [CommRing R] [SMul S R] :
                                        Equations
                                        instance Quaternion.instIsScalarTower {S : Type u_1} {T : Type u_2} {R : Type u_3} [CommRing R] [SMul S T] [SMul S R] [SMul T R] [IsScalarTower S T R] :
                                        Equations
                                        • =
                                        instance Quaternion.instSMulCommClass {S : Type u_1} {T : Type u_2} {R : Type u_3} [CommRing R] [SMul S R] [SMul T R] [SMulCommClass S T R] :
                                        Equations
                                        • =
                                        instance Quaternion.algebra {S : Type u_1} {R : Type u_3} [CommRing R] [CommSemiring S] [Algebra S R] :
                                        Equations
                                        instance Quaternion.instStar {R : Type u_3} [CommRing R] :
                                        Equations
                                        • Quaternion.instStar = QuaternionAlgebra.instStarQuaternionAlgebra
                                        Equations
                                        • Quaternion.instStarRing = QuaternionAlgebra.instStarRing
                                        Equations
                                        • =
                                        theorem Quaternion.ext {R : Type u_3} [CommRing R] (a : Quaternion R) (b : Quaternion R) :
                                        a.re = b.rea.imI = b.imIa.imJ = b.imJa.imK = b.imKa = b
                                        theorem Quaternion.ext_iff {R : Type u_3} [CommRing R] {a : Quaternion R} {b : Quaternion R} :
                                        a = b a.re = b.re a.imI = b.imI a.imJ = b.imJ a.imK = b.imK
                                        def Quaternion.im {R : Type u_3} [CommRing R] (x : Quaternion R) :

                                        The imaginary part of a quaternion.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem Quaternion.im_re {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          a.im.re = 0
                                          @[simp]
                                          theorem Quaternion.im_imI {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          a.im.imI = a.imI
                                          @[simp]
                                          theorem Quaternion.im_imJ {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          a.im.imJ = a.imJ
                                          @[simp]
                                          theorem Quaternion.im_imK {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          a.im.imK = a.imK
                                          @[simp]
                                          theorem Quaternion.im_idem {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          a.im.im = a.im
                                          @[simp]
                                          theorem Quaternion.re_add_im {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          a.re + a.im = a
                                          @[simp]
                                          theorem Quaternion.sub_self_im {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          a - a.im = a.re
                                          @[simp]
                                          theorem Quaternion.sub_self_re {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          a - a.re = a.im
                                          @[simp]
                                          theorem Quaternion.coe_re {R : Type u_3} [CommRing R] (x : R) :
                                          (x).re = x
                                          @[simp]
                                          theorem Quaternion.coe_imI {R : Type u_3} [CommRing R] (x : R) :
                                          (x).imI = 0
                                          @[simp]
                                          theorem Quaternion.coe_imJ {R : Type u_3} [CommRing R] (x : R) :
                                          (x).imJ = 0
                                          @[simp]
                                          theorem Quaternion.coe_imK {R : Type u_3} [CommRing R] (x : R) :
                                          (x).imK = 0
                                          @[simp]
                                          theorem Quaternion.coe_im {R : Type u_3} [CommRing R] (x : R) :
                                          (x).im = 0
                                          @[simp]
                                          theorem Quaternion.zero_re {R : Type u_3} [CommRing R] :
                                          @[simp]
                                          theorem Quaternion.zero_imI {R : Type u_3} [CommRing R] :
                                          @[simp]
                                          theorem Quaternion.zero_imJ {R : Type u_3} [CommRing R] :
                                          @[simp]
                                          theorem Quaternion.zero_imK {R : Type u_3} [CommRing R] :
                                          @[simp]
                                          theorem Quaternion.zero_im {R : Type u_3} [CommRing R] :
                                          @[simp]
                                          theorem Quaternion.coe_zero {R : Type u_3} [CommRing R] :
                                          0 = 0
                                          @[simp]
                                          theorem Quaternion.one_re {R : Type u_3} [CommRing R] :
                                          @[simp]
                                          theorem Quaternion.one_imI {R : Type u_3} [CommRing R] :
                                          @[simp]
                                          theorem Quaternion.one_imJ {R : Type u_3} [CommRing R] :
                                          @[simp]
                                          theorem Quaternion.one_imK {R : Type u_3} [CommRing R] :
                                          @[simp]
                                          theorem Quaternion.one_im {R : Type u_3} [CommRing R] :
                                          @[simp]
                                          theorem Quaternion.coe_one {R : Type u_3} [CommRing R] :
                                          1 = 1
                                          @[simp]
                                          theorem Quaternion.add_re {R : Type u_3} [CommRing R] (a : Quaternion R) (b : Quaternion R) :
                                          (a + b).re = a.re + b.re
                                          @[simp]
                                          theorem Quaternion.add_imI {R : Type u_3} [CommRing R] (a : Quaternion R) (b : Quaternion R) :
                                          (a + b).imI = a.imI + b.imI
                                          @[simp]
                                          theorem Quaternion.add_imJ {R : Type u_3} [CommRing R] (a : Quaternion R) (b : Quaternion R) :
                                          (a + b).imJ = a.imJ + b.imJ
                                          @[simp]
                                          theorem Quaternion.add_imK {R : Type u_3} [CommRing R] (a : Quaternion R) (b : Quaternion R) :
                                          (a + b).imK = a.imK + b.imK
                                          @[simp]
                                          theorem Quaternion.add_im {R : Type u_3} [CommRing R] (a : Quaternion R) (b : Quaternion R) :
                                          (a + b).im = a.im + b.im
                                          @[simp]
                                          theorem Quaternion.coe_add {R : Type u_3} [CommRing R] (x : R) (y : R) :
                                          (x + y) = x + y
                                          @[simp]
                                          theorem Quaternion.neg_re {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          (-a).re = -a.re
                                          @[simp]
                                          theorem Quaternion.neg_imI {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          (-a).imI = -a.imI
                                          @[simp]
                                          theorem Quaternion.neg_imJ {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          (-a).imJ = -a.imJ
                                          @[simp]
                                          theorem Quaternion.neg_imK {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          (-a).imK = -a.imK
                                          @[simp]
                                          theorem Quaternion.neg_im {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          (-a).im = -a.im
                                          @[simp]
                                          theorem Quaternion.coe_neg {R : Type u_3} [CommRing R] (x : R) :
                                          (-x) = -x
                                          @[simp]
                                          theorem Quaternion.sub_re {R : Type u_3} [CommRing R] (a : Quaternion R) (b : Quaternion R) :
                                          (a - b).re = a.re - b.re
                                          @[simp]
                                          theorem Quaternion.sub_imI {R : Type u_3} [CommRing R] (a : Quaternion R) (b : Quaternion R) :
                                          (a - b).imI = a.imI - b.imI
                                          @[simp]
                                          theorem Quaternion.sub_imJ {R : Type u_3} [CommRing R] (a : Quaternion R) (b : Quaternion R) :
                                          (a - b).imJ = a.imJ - b.imJ
                                          @[simp]
                                          theorem Quaternion.sub_imK {R : Type u_3} [CommRing R] (a : Quaternion R) (b : Quaternion R) :
                                          (a - b).imK = a.imK - b.imK
                                          @[simp]
                                          theorem Quaternion.sub_im {R : Type u_3} [CommRing R] (a : Quaternion R) (b : Quaternion R) :
                                          (a - b).im = a.im - b.im
                                          @[simp]
                                          theorem Quaternion.coe_sub {R : Type u_3} [CommRing R] (x : R) (y : R) :
                                          (x - y) = x - y
                                          @[simp]
                                          theorem Quaternion.mul_re {R : Type u_3} [CommRing R] (a : Quaternion R) (b : Quaternion R) :
                                          (a * b).re = a.re * b.re - a.imI * b.imI - a.imJ * b.imJ - a.imK * b.imK
                                          @[simp]
                                          theorem Quaternion.mul_imI {R : Type u_3} [CommRing R] (a : Quaternion R) (b : Quaternion R) :
                                          (a * b).imI = a.re * b.imI + a.imI * b.re + a.imJ * b.imK - a.imK * b.imJ
                                          @[simp]
                                          theorem Quaternion.mul_imJ {R : Type u_3} [CommRing R] (a : Quaternion R) (b : Quaternion R) :
                                          (a * b).imJ = a.re * b.imJ - a.imI * b.imK + a.imJ * b.re + a.imK * b.imI
                                          @[simp]
                                          theorem Quaternion.mul_imK {R : Type u_3} [CommRing R] (a : Quaternion R) (b : Quaternion R) :
                                          (a * b).imK = a.re * b.imK + a.imI * b.imJ - a.imJ * b.imI + a.imK * b.re
                                          @[simp]
                                          theorem Quaternion.coe_mul {R : Type u_3} [CommRing R] (x : R) (y : R) :
                                          (x * y) = x * y
                                          @[simp]
                                          theorem Quaternion.coe_pow {R : Type u_3} [CommRing R] (x : R) (n : ) :
                                          (x ^ n) = x ^ n
                                          @[simp]
                                          theorem Quaternion.natCast_re {R : Type u_3} [CommRing R] (n : ) :
                                          (n).re = n
                                          @[simp]
                                          theorem Quaternion.natCast_imI {R : Type u_3} [CommRing R] (n : ) :
                                          (n).imI = 0
                                          @[simp]
                                          theorem Quaternion.natCast_imJ {R : Type u_3} [CommRing R] (n : ) :
                                          (n).imJ = 0
                                          @[simp]
                                          theorem Quaternion.natCast_imK {R : Type u_3} [CommRing R] (n : ) :
                                          (n).imK = 0
                                          @[simp]
                                          theorem Quaternion.natCast_im {R : Type u_3} [CommRing R] (n : ) :
                                          (n).im = 0
                                          theorem Quaternion.coe_natCast {R : Type u_3} [CommRing R] (n : ) :
                                          n = n
                                          @[simp]
                                          theorem Quaternion.intCast_re {R : Type u_3} [CommRing R] (z : ) :
                                          (z).re = z
                                          @[simp]
                                          theorem Quaternion.intCast_imI {R : Type u_3} [CommRing R] (z : ) :
                                          (z).imI = 0
                                          @[simp]
                                          theorem Quaternion.intCast_imJ {R : Type u_3} [CommRing R] (z : ) :
                                          (z).imJ = 0
                                          @[simp]
                                          theorem Quaternion.intCast_imK {R : Type u_3} [CommRing R] (z : ) :
                                          (z).imK = 0
                                          @[simp]
                                          theorem Quaternion.intCast_im {R : Type u_3} [CommRing R] (z : ) :
                                          (z).im = 0
                                          theorem Quaternion.coe_intCast {R : Type u_3} [CommRing R] (z : ) :
                                          z = z
                                          theorem Quaternion.coe_injective {R : Type u_3} [CommRing R] :
                                          Function.Injective Quaternion.coe
                                          @[simp]
                                          theorem Quaternion.coe_inj {R : Type u_3} [CommRing R] {x : R} {y : R} :
                                          x = y x = y
                                          @[simp]
                                          theorem Quaternion.smul_re {S : Type u_1} {R : Type u_3} [CommRing R] (a : Quaternion R) [SMul S R] (s : S) :
                                          (s a).re = s a.re
                                          @[simp]
                                          theorem Quaternion.smul_imI {S : Type u_1} {R : Type u_3} [CommRing R] (a : Quaternion R) [SMul S R] (s : S) :
                                          (s a).imI = s a.imI
                                          @[simp]
                                          theorem Quaternion.smul_imJ {S : Type u_1} {R : Type u_3} [CommRing R] (a : Quaternion R) [SMul S R] (s : S) :
                                          (s a).imJ = s a.imJ
                                          @[simp]
                                          theorem Quaternion.smul_imK {S : Type u_1} {R : Type u_3} [CommRing R] (a : Quaternion R) [SMul S R] (s : S) :
                                          (s a).imK = s a.imK
                                          @[simp]
                                          theorem Quaternion.smul_im {S : Type u_1} {R : Type u_3} [CommRing R] (a : Quaternion R) [SMulZeroClass S R] (s : S) :
                                          (s a).im = s a.im
                                          @[simp]
                                          theorem Quaternion.coe_smul {S : Type u_1} {R : Type u_3} [CommRing R] [SMulZeroClass S R] (s : S) (r : R) :
                                          (s r) = s r
                                          theorem Quaternion.coe_commutes {R : Type u_3} [CommRing R] (r : R) (a : Quaternion R) :
                                          r * a = a * r
                                          theorem Quaternion.coe_commute {R : Type u_3} [CommRing R] (r : R) (a : Quaternion R) :
                                          Commute (r) a
                                          theorem Quaternion.coe_mul_eq_smul {R : Type u_3} [CommRing R] (r : R) (a : Quaternion R) :
                                          r * a = r a
                                          theorem Quaternion.mul_coe_eq_smul {R : Type u_3} [CommRing R] (r : R) (a : Quaternion R) :
                                          a * r = r a
                                          @[simp]
                                          theorem Quaternion.algebraMap_def {R : Type u_3} [CommRing R] :
                                          (algebraMap R (Quaternion R)) = Quaternion.coe
                                          theorem Quaternion.smul_coe {R : Type u_3} [CommRing R] (x : R) (y : R) :
                                          x y = (x * y)
                                          Equations
                                          • =
                                          Equations
                                          • =
                                          @[simp]
                                          theorem Quaternion.star_re {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          (star a).re = a.re
                                          @[simp]
                                          theorem Quaternion.star_imI {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          (star a).imI = -a.imI
                                          @[simp]
                                          theorem Quaternion.star_imJ {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          (star a).imJ = -a.imJ
                                          @[simp]
                                          theorem Quaternion.star_imK {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          (star a).imK = -a.imK
                                          @[simp]
                                          theorem Quaternion.star_im {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          (star a).im = -a.im
                                          theorem Quaternion.self_add_star' {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          a + star a = (2 * a.re)
                                          theorem Quaternion.self_add_star {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          a + star a = 2 * a.re
                                          theorem Quaternion.star_add_self' {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          star a + a = (2 * a.re)
                                          theorem Quaternion.star_add_self {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          star a + a = 2 * a.re
                                          theorem Quaternion.star_eq_two_re_sub {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          star a = (2 * a.re) - a
                                          @[simp]
                                          theorem Quaternion.star_coe {R : Type u_3} [CommRing R] (x : R) :
                                          star x = x
                                          @[simp]
                                          theorem Quaternion.im_star {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          star a.im = -a.im
                                          @[simp]
                                          theorem Quaternion.star_smul {S : Type u_1} {R : Type u_3} [CommRing R] [Monoid S] [DistribMulAction S R] (s : S) (a : Quaternion R) :
                                          star (s a) = s star a
                                          theorem Quaternion.eq_re_of_eq_coe {R : Type u_3} [CommRing R] {a : Quaternion R} {x : R} (h : a = x) :
                                          a = a.re
                                          theorem Quaternion.eq_re_iff_mem_range_coe {R : Type u_3} [CommRing R] {a : Quaternion R} :
                                          a = a.re a Set.range Quaternion.coe
                                          @[simp]
                                          theorem Quaternion.star_eq_self {R : Type u_3} [CommRing R] [NoZeroDivisors R] [CharZero R] {a : Quaternion R} :
                                          star a = a a = a.re
                                          @[simp]
                                          theorem Quaternion.star_eq_neg {R : Type u_3} [CommRing R] [NoZeroDivisors R] [CharZero R] {a : Quaternion R} :
                                          star a = -a a.re = 0
                                          theorem Quaternion.star_mul_eq_coe {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          star a * a = (star a * a).re
                                          theorem Quaternion.mul_star_eq_coe {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                          a * star a = (a * star a).re

                                          Quaternion conjugate as an AlgEquiv to the opposite ring.

                                          Equations
                                          • Quaternion.starAe = QuaternionAlgebra.starAe
                                          Instances For
                                            @[simp]
                                            theorem Quaternion.coe_starAe {R : Type u_3} [CommRing R] :
                                            Quaternion.starAe = MulOpposite.op star

                                            Square of the norm.

                                            Equations
                                            • Quaternion.normSq = { toFun := fun (a : Quaternion R) => (a * star a).re, map_zero' := , map_one' := , map_mul' := }
                                            Instances For
                                              theorem Quaternion.normSq_def {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                              Quaternion.normSq a = (a * star a).re
                                              theorem Quaternion.normSq_def' {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                              Quaternion.normSq a = a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2
                                              theorem Quaternion.normSq_coe {R : Type u_3} [CommRing R] (x : R) :
                                              Quaternion.normSq x = x ^ 2
                                              @[simp]
                                              theorem Quaternion.normSq_star {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                              Quaternion.normSq (star a) = Quaternion.normSq a
                                              theorem Quaternion.normSq_natCast {R : Type u_3} [CommRing R] (n : ) :
                                              Quaternion.normSq n = n ^ 2
                                              theorem Quaternion.normSq_intCast {R : Type u_3} [CommRing R] (z : ) :
                                              Quaternion.normSq z = z ^ 2
                                              @[simp]
                                              theorem Quaternion.normSq_neg {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                              Quaternion.normSq (-a) = Quaternion.normSq a
                                              theorem Quaternion.self_mul_star {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                              a * star a = (Quaternion.normSq a)
                                              theorem Quaternion.star_mul_self {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                              star a * a = (Quaternion.normSq a)
                                              theorem Quaternion.im_sq {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                              a.im ^ 2 = -(Quaternion.normSq a.im)
                                              theorem Quaternion.coe_normSq_add {R : Type u_3} [CommRing R] (a : Quaternion R) (b : Quaternion R) :
                                              (Quaternion.normSq (a + b)) = (Quaternion.normSq a) + a * star b + b * star a + (Quaternion.normSq b)
                                              theorem Quaternion.normSq_smul {R : Type u_3} [CommRing R] (r : R) (q : Quaternion R) :
                                              Quaternion.normSq (r q) = r ^ 2 * Quaternion.normSq q
                                              theorem Quaternion.normSq_add {R : Type u_3} [CommRing R] (a : Quaternion R) (b : Quaternion R) :
                                              Quaternion.normSq (a + b) = Quaternion.normSq a + Quaternion.normSq b + 2 * (a * star b).re
                                              @[simp]
                                              theorem Quaternion.normSq_eq_zero {R : Type u_1} [LinearOrderedCommRing R] {a : Quaternion R} :
                                              Quaternion.normSq a = 0 a = 0
                                              theorem Quaternion.normSq_ne_zero {R : Type u_1} [LinearOrderedCommRing R] {a : Quaternion R} :
                                              Quaternion.normSq a 0 a 0
                                              @[simp]
                                              theorem Quaternion.normSq_nonneg {R : Type u_1} [LinearOrderedCommRing R] {a : Quaternion R} :
                                              0 Quaternion.normSq a
                                              @[simp]
                                              theorem Quaternion.normSq_le_zero {R : Type u_1} [LinearOrderedCommRing R] {a : Quaternion R} :
                                              Quaternion.normSq a 0 a = 0
                                              Equations
                                              • =
                                              theorem Quaternion.sq_eq_normSq {R : Type u_1} [LinearOrderedCommRing R] {a : Quaternion R} :
                                              a ^ 2 = (Quaternion.normSq a) a = a.re
                                              theorem Quaternion.sq_eq_neg_normSq {R : Type u_1} [LinearOrderedCommRing R] {a : Quaternion R} :
                                              a ^ 2 = -(Quaternion.normSq a) a.re = 0
                                              theorem Quaternion.instInv_inv {R : Type u_1} [LinearOrderedField R] (a : Quaternion R) :
                                              a⁻¹ = (Quaternion.normSq a)⁻¹ star a
                                              Equations
                                              Equations
                                              • Quaternion.instGroupWithZero = let __src := ; let __src_1 := inferInstance; GroupWithZero.mk zpowRec
                                              @[simp]
                                              theorem Quaternion.coe_inv {R : Type u_1} [LinearOrderedField R] (x : R) :
                                              x⁻¹ = (x)⁻¹
                                              @[simp]
                                              theorem Quaternion.coe_div {R : Type u_1} [LinearOrderedField R] (x : R) (y : R) :
                                              (x / y) = x / y
                                              @[simp]
                                              theorem Quaternion.coe_zpow {R : Type u_1} [LinearOrderedField R] (x : R) (z : ) :
                                              (x ^ z) = x ^ z
                                              Equations
                                              • Quaternion.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => q }
                                              Equations
                                              • Quaternion.instRatCast = { ratCast := fun (q : ) => q }
                                              @[simp]
                                              theorem Quaternion.re_nnratCast {R : Type u_1} [LinearOrderedField R] (q : ℚ≥0) :
                                              (q).re = q
                                              @[simp]
                                              theorem Quaternion.im_nnratCast {R : Type u_1} [LinearOrderedField R] (q : ℚ≥0) :
                                              (q).im = 0
                                              @[simp]
                                              theorem Quaternion.imI_nnratCast {R : Type u_1} [LinearOrderedField R] (q : ℚ≥0) :
                                              (q).imI = 0
                                              @[simp]
                                              theorem Quaternion.imJ_nnratCast {R : Type u_1} [LinearOrderedField R] (q : ℚ≥0) :
                                              (q).imJ = 0
                                              @[simp]
                                              theorem Quaternion.imK_nnratCast {R : Type u_1} [LinearOrderedField R] (q : ℚ≥0) :
                                              (q).imK = 0
                                              @[simp]
                                              theorem Quaternion.ratCast_re {R : Type u_1} [LinearOrderedField R] (q : ) :
                                              (q).re = q
                                              @[simp]
                                              theorem Quaternion.ratCast_im {R : Type u_1} [LinearOrderedField R] (q : ) :
                                              (q).im = 0
                                              @[simp]
                                              theorem Quaternion.ratCast_imI {R : Type u_1} [LinearOrderedField R] (q : ) :
                                              (q).imI = 0
                                              @[simp]
                                              theorem Quaternion.ratCast_imJ {R : Type u_1} [LinearOrderedField R] (q : ) :
                                              (q).imJ = 0
                                              @[simp]
                                              theorem Quaternion.ratCast_imK {R : Type u_1} [LinearOrderedField R] (q : ) :
                                              (q).imK = 0
                                              theorem Quaternion.coe_nnratCast {R : Type u_1} [LinearOrderedField R] (q : ℚ≥0) :
                                              q = q
                                              theorem Quaternion.coe_ratCast {R : Type u_1} [LinearOrderedField R] (q : ) :
                                              q = q
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              theorem Quaternion.normSq_inv {R : Type u_1} [LinearOrderedField R] (a : Quaternion R) :
                                              Quaternion.normSq a⁻¹ = (Quaternion.normSq a)⁻¹
                                              theorem Quaternion.normSq_div {R : Type u_1} [LinearOrderedField R] (a : Quaternion R) (b : Quaternion R) :
                                              Quaternion.normSq (a / b) = Quaternion.normSq a / Quaternion.normSq b
                                              theorem Quaternion.normSq_zpow {R : Type u_1} [LinearOrderedField R] (a : Quaternion R) (z : ) :
                                              Quaternion.normSq (a ^ z) = Quaternion.normSq a ^ z
                                              theorem Quaternion.normSq_ratCast {R : Type u_1} [LinearOrderedField R] (q : ) :
                                              (Quaternion.normSq q) = q ^ 2
                                              theorem Cardinal.mk_quaternionAlgebra {R : Type u_1} (c₁ : R) (c₂ : R) :

                                              The cardinality of a quaternion algebra, as a type.

                                              @[simp]
                                              theorem Cardinal.mk_quaternionAlgebra_of_infinite {R : Type u_1} (c₁ : R) (c₂ : R) [Infinite R] :
                                              theorem Cardinal.mk_univ_quaternionAlgebra {R : Type u_1} (c₁ : R) (c₂ : R) :
                                              Cardinal.mk Set.univ = Cardinal.mk R ^ 4

                                              The cardinality of a quaternion algebra, as a set.

                                              theorem Cardinal.mk_univ_quaternionAlgebra_of_infinite {R : Type u_1} (c₁ : R) (c₂ : R) [Infinite R] :
                                              Cardinal.mk Set.univ = Cardinal.mk R
                                              @[simp]

                                              The cardinality of the quaternions, as a type.

                                              theorem Cardinal.mk_univ_quaternion (R : Type u_1) [One R] [Neg R] :
                                              Cardinal.mk Set.univ = Cardinal.mk R ^ 4

                                              The cardinality of the quaternions, as a set.