Theorems · Theorem · ring theory

QuaternionAlgebra.Basis.i_mul_j

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

Defined in

Mathlib.Algebra.QuaternionBasis

Cited by

6 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

CommRingRingAlgebra