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
  • re : R

    Real part of a quaternion.

  • imI : R
  • imJ : R
  • imK : R

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.

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.

    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_imJ {R : Type u_1} (c₁ : R) (c₂ : R) (a : R × R × R × R) :
      ((QuaternionAlgebra.equivProd c₁ c₂).symm a).imJ = a.snd.snd.fst
      @[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.snd.snd.snd
      @[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.fst
      @[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.snd.fst
      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.

      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.

        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
          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.

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

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

            Instances For
              instance QuaternionAlgebra.instCoeTCQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              CoeTC R (QuaternionAlgebra R c₁ c₂)
              @[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.instZeroQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              Zero (QuaternionAlgebra R c₁ c₂)
              @[simp]
              theorem QuaternionAlgebra.zero_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              0.re = 0
              @[simp]
              theorem QuaternionAlgebra.zero_imI {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              0.imI = 0
              @[simp]
              theorem QuaternionAlgebra.zero_imJ {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              0.imJ = 0
              @[simp]
              theorem QuaternionAlgebra.zero_imK {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              0.imK = 0
              @[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.instInhabitedQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              instance QuaternionAlgebra.instOneQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              One (QuaternionAlgebra R c₁ c₂)
              @[simp]
              theorem QuaternionAlgebra.one_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              1.re = 1
              @[simp]
              theorem QuaternionAlgebra.one_imI {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              1.imI = 0
              @[simp]
              theorem QuaternionAlgebra.one_imJ {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              1.imJ = 0
              @[simp]
              theorem QuaternionAlgebra.one_imK {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              1.imK = 0
              @[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.instAddQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              Add (QuaternionAlgebra R c₁ c₂)
              @[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₂) :
              @[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.instNegQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              Neg (QuaternionAlgebra R c₁ c₂)
              @[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₂) :
              @[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.instSubQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :
              Sub (QuaternionAlgebra R c₁ c₂)
              @[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₂) :
              @[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) :
              @[simp]
              theorem QuaternionAlgebra.re_add_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
              @[simp]
              theorem QuaternionAlgebra.sub_self_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
              @[simp]
              theorem QuaternionAlgebra.sub_self_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
              instance QuaternionAlgebra.instMulQuaternionAlgebra {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.
              @[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.instSMulQuaternionAlgebra {S : Type u_1} {R : Type u_3} {c₁ : R} {c₂ : R} [SMul S R] :
              SMul S (QuaternionAlgebra R c₁ c₂)
              @[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) :
              @[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
              @[simp]
              theorem QuaternionAlgebra.nat_cast_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (n : ) :
              (n).re = n
              @[simp]
              theorem QuaternionAlgebra.nat_cast_imI {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (n : ) :
              (n).imI = 0
              @[simp]
              theorem QuaternionAlgebra.nat_cast_imJ {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (n : ) :
              (n).imJ = 0
              @[simp]
              theorem QuaternionAlgebra.nat_cast_imK {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (n : ) :
              (n).imK = 0
              @[simp]
              theorem QuaternionAlgebra.nat_cast_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (n : ) :
              theorem QuaternionAlgebra.coe_nat_cast {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (n : ) :
              n = n
              @[simp]
              theorem QuaternionAlgebra.int_cast_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (z : ) :
              (z).re = z
              @[simp]
              theorem QuaternionAlgebra.int_cast_imI {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (z : ) :
              (z).imI = 0
              @[simp]
              theorem QuaternionAlgebra.int_cast_imJ {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (z : ) :
              (z).imJ = 0
              @[simp]
              theorem QuaternionAlgebra.int_cast_imK {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (z : ) :
              (z).imK = 0
              @[simp]
              theorem QuaternionAlgebra.int_cast_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (z : ) :
              theorem QuaternionAlgebra.coe_int_cast {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₂)
              @[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.instAlgebraQuaternionAlgebraToSemiringInstRing {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₂)
              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 }
              @[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

              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

                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

                  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

                    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.

                      Instances For
                        @[simp]
                        theorem QuaternionAlgebra.coe_linearEquivTuple {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) :
                        @[simp]
                        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.

                        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]
                          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.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.

                          @[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₂) :
                          @[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} :
                          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
                          @[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₂) :
                          @[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.

                          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.

                            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.snd.fst
                              @[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.snd.snd.snd
                              @[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.fst
                              @[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.snd.snd.fst
                              @[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)
                              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.

                              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.

                                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]
                                  def Quaternion.coe {R : Type u_3} [CommRing R] :
                                  RQuaternion R

                                  Coercion R → ℍ[R].

                                  Instances For
                                    instance Quaternion.algebra {S : Type u_1} {R : Type u_3} [CommRing R] [CommSemiring S] [Algebra S R] :
                                    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.

                                    Instances For
                                      @[simp]
                                      theorem Quaternion.im_re {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                      (Quaternion.im a).re = 0
                                      @[simp]
                                      theorem Quaternion.im_imI {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                      (Quaternion.im a).imI = a.imI
                                      @[simp]
                                      theorem Quaternion.im_imJ {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                      (Quaternion.im a).imJ = a.imJ
                                      @[simp]
                                      theorem Quaternion.im_imK {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                      (Quaternion.im a).imK = a.imK
                                      @[simp]
                                      theorem Quaternion.re_add_im {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                      a.re + Quaternion.im a = a
                                      @[simp]
                                      theorem Quaternion.sub_self_im {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                      a - Quaternion.im a = a.re
                                      @[simp]
                                      theorem Quaternion.sub_self_re {R : Type u_3} [CommRing R] (a : Quaternion R) :
                                      a - a.re = Quaternion.im a
                                      @[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) :
                                      @[simp]
                                      theorem Quaternion.zero_re {R : Type u_3} [CommRing R] :
                                      0.re = 0
                                      @[simp]
                                      theorem Quaternion.zero_imI {R : Type u_3} [CommRing R] :
                                      0.imI = 0
                                      @[simp]
                                      theorem Quaternion.zero_imJ {R : Type u_3} [CommRing R] :
                                      0.imJ = 0
                                      @[simp]
                                      theorem Quaternion.zero_imK {R : Type u_3} [CommRing R] :
                                      0.imK = 0
                                      @[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] :
                                      1.re = 1
                                      @[simp]
                                      theorem Quaternion.one_imI {R : Type u_3} [CommRing R] :
                                      1.imI = 0
                                      @[simp]
                                      theorem Quaternion.one_imJ {R : Type u_3} [CommRing R] :
                                      1.imJ = 0
                                      @[simp]
                                      theorem Quaternion.one_imK {R : Type u_3} [CommRing R] :
                                      1.imK = 0
                                      @[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]
                                      @[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]
                                      @[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]
                                      @[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.nat_cast_re {R : Type u_3} [CommRing R] (n : ) :
                                      (n).re = n
                                      @[simp]
                                      theorem Quaternion.nat_cast_imI {R : Type u_3} [CommRing R] (n : ) :
                                      (n).imI = 0
                                      @[simp]
                                      theorem Quaternion.nat_cast_imJ {R : Type u_3} [CommRing R] (n : ) :
                                      (n).imJ = 0
                                      @[simp]
                                      theorem Quaternion.nat_cast_imK {R : Type u_3} [CommRing R] (n : ) :
                                      (n).imK = 0
                                      @[simp]
                                      theorem Quaternion.nat_cast_im {R : Type u_3} [CommRing R] (n : ) :
                                      theorem Quaternion.coe_nat_cast {R : Type u_3} [CommRing R] (n : ) :
                                      n = n
                                      @[simp]
                                      theorem Quaternion.int_cast_re {R : Type u_3} [CommRing R] (z : ) :
                                      (z).re = z
                                      @[simp]
                                      theorem Quaternion.int_cast_imI {R : Type u_3} [CommRing R] (z : ) :
                                      (z).imI = 0
                                      @[simp]
                                      theorem Quaternion.int_cast_imJ {R : Type u_3} [CommRing R] (z : ) :
                                      (z).imJ = 0
                                      @[simp]
                                      theorem Quaternion.int_cast_imK {R : Type u_3} [CommRing R] (z : ) :
                                      (z).imK = 0
                                      @[simp]
                                      theorem Quaternion.int_cast_im {R : Type u_3} [CommRing R] (z : ) :
                                      theorem Quaternion.coe_int_cast {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) :
                                      @[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)
                                      @[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.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]
                                      @[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.

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

                                        Square of the norm.

                                        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_nat_cast {R : Type u_3} [CommRing R] (n : ) :
                                          Quaternion.normSq n = n ^ 2
                                          theorem Quaternion.normSq_int_cast {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) :
                                          Quaternion.im a ^ 2 = -↑(Quaternion.normSq (Quaternion.im a))
                                          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
                                          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
                                          @[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
                                          @[simp]
                                          theorem Quaternion.rat_cast_re {R : Type u_1} [LinearOrderedField R] (q : ) :
                                          (q).re = q
                                          @[simp]
                                          theorem Quaternion.rat_cast_imI {R : Type u_1} [LinearOrderedField R] (q : ) :
                                          (q).imI = 0
                                          @[simp]
                                          theorem Quaternion.rat_cast_imJ {R : Type u_1} [LinearOrderedField R] (q : ) :
                                          (q).imJ = 0
                                          @[simp]
                                          theorem Quaternion.rat_cast_imK {R : Type u_1} [LinearOrderedField R] (q : ) :
                                          (q).imK = 0
                                          @[simp]
                                          theorem Quaternion.rat_cast_im {R : Type u_1} [LinearOrderedField R] (q : ) :
                                          theorem Quaternion.coe_rat_cast {R : Type u_1} [LinearOrderedField R] (q : ) :
                                          q = q
                                          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_rat_cast {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.