QuaternionAlgebra.coe_mul
theorem QuaternionAlgebra.coe_mul : ∀ {R : Type u_3} [inst : CommRing R] {c₁ c₂ : R} (x y : R), ↑(x * y) = ↑x * ↑y := by
sorry
This theorem states that for any commutative ring `R` and any elements `c₁`, `c₂`, `x`, and `y` of `R`, the quaternion algebra operation of converting the product `x * y` to a quaternion preserves the multiplication operation. In other words, converting `x * y` to a quaternion gives the same result as converting `x` and `y` to quaternions and then multiplying them. Mathematically speaking, it says that for any `x` and `y` in the ring, `↑(x * y) = ↑x * ↑y`, where `↑` denotes the quaternion algebra operation.
More concisely: For any commutative ring `R` and elements `x, y` in `R`, the quaternion algebra operation `↑` satisfies `↑(x * y) = ↑x * ↑y`.
|
Quaternion.normSq_coe
theorem Quaternion.normSq_coe : ∀ {R : Type u_3} [inst : CommRing R] (x : R), Quaternion.normSq ↑x = x ^ 2
This theorem states that for any type `R` that forms a commutative ring, the square of the norm of the quaternion formed by taking the "coercion" (or type conversion) of a value `x` from `R` is equal to the square of `x`. In other words, when we convert a number from the ring `R` to a quaternion and calculate the square of its norm, we get the same result as squaring the original number in `R`.
More concisely: For any commutative ring `R` and any `x` in `R`, the square of the norm of the quaternion obtained by coercing `x` equals `x`'s square in `R`.
|
Cardinal.mk_quaternionAlgebra
theorem Cardinal.mk_quaternionAlgebra :
∀ {R : Type u_1} (c₁ c₂ : R), Cardinal.mk (QuaternionAlgebra R c₁ c₂) = Cardinal.mk R ^ 4
This theorem states that for any type `R` and any two elements `c₁` and `c₂` of `R`, the cardinality of the type of quaternion algebras over `R` with coefficients `c₁` and `c₂` is equal to the fourth power of the cardinality of `R`. In other words, the number of distinct quaternion algebras you can construct over `R` with specific coefficients `c₁` and `c₂` is the same as the number of distinct elements in `R` raised to the fourth power.
More concisely: The number of quaternion algebras over a type `R` with coefficients `c₁` and `c₂` is equal to the fourth power of the cardinality of `R`.
|
Quaternion.ext
theorem Quaternion.ext :
∀ {R : Type u_3} [inst : CommRing R] (a b : Quaternion R),
a.re = b.re → a.imI = b.imI → a.imJ = b.imJ → a.imK = b.imK → a = b
This theorem is stating that for any commutative ring `R` and any two quaternions `a` and `b` over this ring, if the real part of `a` equals the real part of `b`, the coefficient of `i` in `a` equals the coefficient of `i` in `b`, the coefficient of `j` in `a` equals the coefficient of `j` in `b`, and the coefficient of `k` in `a` equals the coefficient of `k` in `b`, then `a` and `b` must be the same quaternion. This is essentially saying that two quaternions are equal if and only if their corresponding components are equal.
More concisely: Given a commutative ring `R`, if for any two quaternions `a` and `b` over `R` with equal real parts and identical coefficients of `i`, `j`, and `k`, then `a` and `b` are equal.
|
QuaternionAlgebra.im_star
theorem QuaternionAlgebra.im_star :
∀ {R : Type u_3} [inst : CommRing R] {c₁ c₂ : R} (a : QuaternionAlgebra R c₁ c₂), (star a).im = -a.im
This theorem states that for any commutative ring `R` and any quaternion `a` in the Quaternion Algebra over `R` with coefficients `c₁` and `c₂`, the imaginary part of the conjugate of `a` (denoted `star a`) is equal to the negation of the imaginary part of `a`. In mathematical terms, it states that `Im(a*) = -Im(a)`, where `a*` denotes the conjugate of a quaternion `a`, `Im` denotes the imaginary part of a quaternion, and `-` denotes negation in the ring `R`.
More concisely: The imaginary part of the conjugate of a quaternion is the negation of its imaginary part.
|
Cardinal.mk_univ_quaternion
theorem Cardinal.mk_univ_quaternion :
∀ (R : Type u_1) [inst : One R] [inst_1 : Neg R], Cardinal.mk ↑Set.univ = Cardinal.mk R ^ 4
This theorem states that the cardinality of the set of quaternions, denoted as `Cardinal.mk ↑Set.univ`, is equal to the cardinality of any arbitrary type `R` raised to the power of 4, given that `R` has a defined identity for multiplication operation (`One R`) and supports negation (`Neg R`). In layman's terms, if you can define an identity for multiplication and a negation on a type, then the number of all possible quaternions you can create from that type is equal to the number of elements in that type raised to the power of 4.
More concisely: If `R` is a type with defined multiplication identity `One R` and negation `Neg R`, then the cardinality of the set of quaternions `{a + bi + jc + kd | a, b, c, d ∈ R}` is equal to `(Cardinal.mk (Set.univ : Set))^4`.
|
Cardinal.mk_quaternion
theorem Cardinal.mk_quaternion :
∀ (R : Type u_1) [inst : One R] [inst_1 : Neg R], Cardinal.mk (Quaternion R) = Cardinal.mk R ^ 4
This theorem states that for any type `R` that has a multiplicative identity and supports negation, the cardinality (or size) of the set of all quaternions over `R` is equal to the fourth power of the cardinality of `R`. In other words, there are exactly |R|^4 different quaternions that can be formed using values from `R`.
More concisely: The number of quaternions with coefficients in a type `R` having a multiplicative identity and supporting negation is equal to the fourth power of the cardinality of `R`.
|
QuaternionAlgebra.coe_mul_eq_smul
theorem QuaternionAlgebra.coe_mul_eq_smul :
∀ {R : Type u_3} [inst : CommRing R] {c₁ c₂ : R} (r : R) (a : QuaternionAlgebra R c₁ c₂), ↑r * a = r • a
This theorem states that for any commutative ring `R` and any elements `c₁`, `c₂`, and `r` of `R`, along with any element `a` of the Quaternion Algebra `QuaternionAlgebra R c₁ c₂`, the product of the coe function applied to `r` and `a` is equal to `r` scalar-multiplied by `a`. In other words, it says that for a quaternion algebra, multiplication by a scalar from the underlying commutative ring can be done by either multiplying by the ring element or scalar multiplication, and these two operations are equivalent.
More concisely: For any commutative ring `R`, any quaternion algebra `a` in `QuaternionAlgebra R c₁ c₂`, and any scalar `r` in `R`, the product of `r` with `a` via scalar multiplication and via the `coe` function application is equal.
|
Quaternion.mul_re
theorem Quaternion.mul_re :
∀ {R : Type u_3} [inst : CommRing R] (a b : Quaternion R),
(a * b).re = a.re * b.re - a.imI * b.imI - a.imJ * b.imJ - a.imK * b.imK
This theorem states that for any commutative ring `R` and any two quaternions `a` and `b` over `R`, the real part (`re`) of the product of `a` and `b` is calculated as the product of their real parts minus the product of their i-component imaginary parts, minus the product of their j-component imaginary parts, minus the product of their k-component imaginary parts. This is essentially the multiplication rule for quaternions.
More concisely: For any commutative ring `R` and quaternions `a` and `b` over `R`, the real part of their product `(a * b).re` is equal to `(a.re * b.re) - (a.i * b.i) - (a.j * b.j) - (a.k * b.k)`.
|
QuaternionAlgebra.ext
theorem QuaternionAlgebra.ext :
∀ {R : Type u_1} {a b : R} (x y : QuaternionAlgebra R a b),
x.re = y.re → x.imI = y.imI → x.imJ = y.imJ → x.imK = y.imK → x = y
This theorem, named `QuaternionAlgebra.ext`, states that for any given ring `R` and any two elements `a` and `b` of `R`, if we have two quaternions `x` and `y` of the Quaternion Algebra defined over `R` with `a` and `b`, and the real part of `x` equals the real part of `y`, the `i` imaginary part of `x` equals the `i` imaginary part of `y`, the `j` imaginary part of `x` equals the `j` imaginary part of `y`, and the `k` imaginary part of `x` equals the `k` imaginary part of `y`, then `x` and `y` are indeed the same quaternion. This is essentially the criteria for equality in the Quaternion Algebra.
More concisely: If two quaternions of the Quaternion Algebra over a ring have equal real and imaginary parts, they are equal.
|
Quaternion.coe_mul_eq_smul
theorem Quaternion.coe_mul_eq_smul : ∀ {R : Type u_3} [inst : CommRing R] (r : R) (a : Quaternion R), ↑r * a = r • a
This theorem states that for any type `R` that forms a commutative ring (denoted by `CommRing R`), and for any real number `r` within that type `R` and any quaternion `a` over type `R` (i.e., `a` is a quaternion whose components are elements of `R`), the operation of multiplying the real number `r` (coerced to a quaternion using the `↑r` notation) with the quaternion `a` (expressed as `↑r * a`) is equivalent to the operation of scaling the quaternion `a` by the real number `r` (expressed as `r • a`). In other words, for any commutative ring `R`, the multiplication of a real number and a quaternion is the same as the scalar multiplication of that real number and the quaternion.
More concisely: For any commutative ring `R`, the multiplication of a real number `r` in `R` with a quaternion `a` over `R` is equivalent to scaling the quaternion `a` by the real number `r`.
|
Quaternion.coe_re
theorem Quaternion.coe_re : ∀ {R : Type u_3} [inst : CommRing R] (x : R), (↑x).re = x
This theorem states that for any commutative ring `R` and any element `x` from `R`, when `x` is cast to a quaternion, the real part of this quaternion is equal to `x`. In other words, it states that the real part of a quaternion, created by lifting an element from a commutative ring, is exactly that element.
More concisely: For any commutative ring `R` and its element `x`, the real part of the quaternion obtained from `x` equals `x`.
|
Quaternion.coe_mul
theorem Quaternion.coe_mul : ∀ {R : Type u_3} [inst : CommRing R] (x y : R), ↑(x * y) = ↑x * ↑y
This theorem states that for any commutative ring `R` and any two elements `x` and `y` from `R`, the quaternionic representation of the product `x * y` is equal to the product of the quaternionic representations of `x` and `y`. In other words, multiplication in the ring `R` is compatible with the quaternionic representation.
More concisely: For any commutative ring R and all its elements x, y, the quaternionic representation of x * y equals the product of the quaternionic representations of x and y.
|
Quaternion.normSq_eq_zero
theorem Quaternion.normSq_eq_zero :
∀ {R : Type u_1} [inst : LinearOrderedCommRing R] {a : Quaternion R}, Quaternion.normSq a = 0 ↔ a = 0
This theorem states that for any quaternion `a` over a type `R`, where `R` is a linearly ordered commutative ring, the square of the norm of `a` is equal to zero if and only if `a` is the zero quaternion. In other words, a quaternion `a` has zero norm squared if and only if it is the zero quaternion, and conversely, if a quaternion `a` is the zero quaternion, then its norm squared is zero. This is a two-way implication theorem that links the zero quaternion with a zero norm square in the space of quaternions over a linearly ordered commutative ring.
More concisely: For any quaternion `a` over a linearly ordered commutative ring `R`, the square of its norm is equal to zero if and only if `a` is the zero quaternion.
|
QuaternionAlgebra.self_add_star'
theorem QuaternionAlgebra.self_add_star' :
∀ {R : Type u_3} [inst : CommRing R] {c₁ c₂ : R} (a : QuaternionAlgebra R c₁ c₂), a + star a = ↑(2 * a.re) := by
sorry
This theorem states that for any instance `a` of the QuaternionAlgebra over a commutative ring `R` with coefficients `c₁` and `c₂`, the sum of `a` and its conjugate (denoted by `star a`) equals two times the real part of `a`. This is denoted as `↑(2 * a.re)`, where `↑` is the coercion function from `R` to QuaternionAlgebra. Essentially, this theorem formalizes a specific property of quaternion algebra concerning the sum of a quaternion and its conjugate in terms of its real part.
More concisely: For any quaternion `a` in the QuaternionAlgebra over a commutative ring with real and imaginary parts `r` and `i`, respectively, the sum of `a` and its conjugate `(r + i * i − j * j − k * k) * a.conj` equals twice the real part `r` of `a`.
|
Quaternion.normSq_def'
theorem Quaternion.normSq_def' :
∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R),
Quaternion.normSq a = a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2
This theorem states that for any Quaternion `a` over a Commutative Ring `R`, the square of the norm of `a` is equal to the sum of squares of the real part of `a`, the coefficient of `i` in `a`, the coefficient of `j` in `a`, and the coefficient of `k` in `a`. That is, if a Quaternion `a` is understood as a + bi + cj + dk, then the square of its norm is a² + b² + c² + d². This theorem is a formalization of the calculation of the square of the norm (magnitude squared) of a quaternion in the mathematical field of Quaternion Algebra.
More concisely: For any quaternion a over a commutative ring, the norm of a squared equals the sum of the squares of its real and imaginary parts.
|
Mathlib.Algebra.Quaternion._auxLemma.6
theorem Mathlib.Algebra.Quaternion._auxLemma.6 :
∀ {R : Type u_1} {a b : R} (x y : QuaternionAlgebra R a b),
(x = y) = (x.re = y.re ∧ x.imI = y.imI ∧ x.imJ = y.imJ ∧ x.imK = y.imK)
This theorem, `Mathlib.Algebra.Quaternion._auxLemma.6`, states that for any given type `R` and any two elements `a` and `b` of `R`, and for any two elements `x` and `y` of the Quaternion Algebra of `R` with coefficients `a` and `b`, `x` is equal to `y` if and only if the real part of `x` is equal to the real part of `y`, the 'i' imaginary part of `x` is equal to the 'i' imaginary part of `y`, the 'j' imaginary part of `x` is equal to the 'j' imaginary part of `y`, and the 'k' imaginary part of `x` is equal to the 'k' imaginary part of `y`.
More concisely: Two quaternions of type `R` with real and imaginary parts `(xℜ, xI, xJ, xK)` and `(yℜ, yI, yJ, yK)` are equal if and only if their real parts are equal and their corresponding imaginary parts are equal.
|
QuaternionAlgebra.coe_add
theorem QuaternionAlgebra.coe_add : ∀ {R : Type u_3} [inst : CommRing R] {c₁ c₂ : R} (x y : R), ↑(x + y) = ↑x + ↑y := by
sorry
This theorem states that for any commutative ring `R` and any two elements `c₁` and `c₂` of `R`, the addition operation in `R` is preserved under the quaternion algebra embedding. Specifically, if `x` and `y` are two elements of `R`, then the quaternion algebra embedding of their sum `x + y` is equal to the sum of their quaternion algebra embeddings `↑x + ↑y`.
More concisely: For any commutative ring `R` and elements `c₁, c₂` of `R`, the quaternion algebra embedding maps the sum `c₁ + c₂` to the sum of their embeddings, i.e., `↑(c₁ + c₂) = ↑c₁ + ↑c₂`.
|
QuaternionAlgebra.coe_commutes
theorem QuaternionAlgebra.coe_commutes :
∀ {R : Type u_3} [inst : CommRing R] {c₁ c₂ : R} (r : R) (a : QuaternionAlgebra R c₁ c₂), ↑r * a = a * ↑r := by
sorry
This theorem states that for any commutative ring `R` and any elements `c₁`, `c₂`, and `r` of `R`, and any quaternion `a` in the quaternion algebra constructed over `R` with `c₁` and `c₂`, the multiplication of `r` (coerced to the quaternion algebra) and `a` is commutative. In other words, `r` times `a` is equal to `a` times `r`.
More concisely: For any commutative ring `R`, any quaternion `a` in the quaternion algebra over `R` with basis `1, i, j, k` and any element `r` in `R`, we have `r * a = a * r`.
|
Cardinal.mk_univ_quaternionAlgebra
theorem Cardinal.mk_univ_quaternionAlgebra : ∀ {R : Type u_1} (c₁ c₂ : R), Cardinal.mk ↑Set.univ = Cardinal.mk R ^ 4
This theorem states that for any type `R` and any two elements `c₁`, `c₂` of `R`, the cardinality (number of elements) of the set of all quaternion algebras over `R` with coefficients `c₁` and `c₂` is equal to the cardinality of `R` raised to the power of 4. In other words, there are exactly `Cardinal.mk R ^ 4` different quaternion algebras over `R` for given coefficients `c₁` and `c₂`.
More concisely: For any type `R` and elements `c₁`, `c₂` in `R`, the number of quaternion algebras over `R` with coefficients `c₁` and `c₂` is equal to the fourth power of the cardinality of `R`.
|