instNontrivial — Mathlib

English

The quaternion algebra ℍ[R] over a field R is nontrivial; there exist distinct elements (e.g., 0 and 1) in ℍ[R].

Русский

Алгебра квадрота ℍ[R] над полем R является нетривиальной: существуют различающиеся элементы, например 0 и 1, в ℍ[R].

LaTeX

$$∃ a,b ∈ ℍ[R], a ≠ b$$

Lean4

instance instNontrivial : Nontrivial ℍ[R] where
  exists_pair_ne := ⟨0, 1, mt (congr_arg QuaternionAlgebra.re) zero_ne_one⟩

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