English
If two quaternion bases have equal i-component and equal j-component, then the bases are equal.
Русский
Если две базы кватернионной алгебры имеют одинаковые i- и j-компоненты, то базы равны.
LaTeX
$$Ext \text{ for basis }: if q1.i = q2.i and q1.j = q2.j then q1 = q2$$
Lean4
/-- Since `k` is redundant, it is not necessary to show `q₁.k = q₂.k` when showing `q₁ = q₂`. -/
@[ext]
protected theorem ext ⦃q₁ q₂ : Basis A c₁ c₂ c₃⦄ (hi : q₁.i = q₂.i) (hj : q₁.j = q₂.j) : q₁ = q₂ := by cases q₁;
cases q₂; grind