Theorems · Theorem · ring theory

QuaternionAlgebra.Basis.ext

∀ {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₁ q₂ : QuaternionAlgebra.Basis A c₁ c₂ c₃⦄, q₁.i = q₂.i → q₁.j = q₂.j → q₁ = q₂

Since k is redundant, it is not necessary to show q₁.k = q₂.k when showing q₁ = q₂.

Defined in

Mathlib.Algebra.QuaternionBasis

Cited by

2 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingRingAlgebra