Theorems · Theorem · ring theory

QuaternionAlgebra.Basis.j_mul_k

∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (q : QuaternionAlgebra.Basis A c₁ c₂ c₃), q.j * q.k = (c₂ * c₃) • 1 - c₃ • q.i

Defined in

Mathlib.Algebra.QuaternionBasis

Cited by

1 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Quot.sound

Assumes

CommRingRingAlgebra