ext — Mathlib

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

Похожие утверждения