instNoZeroSMulDivisorsOfNoZeroDivisors

English

If R has no zero divisors, then the quaternion algebra ℍ[R,c1,c2,c3] has no zero-smul-divisors: if t ≠ 0 and t ⋅ q = 0 then q = 0 for q ∈ ℍ.

Русский

Если R не имеет нулевых делителей, то ℍ[R,c1,c2,c3] имеет свойство без нулевых делителей скалярного умножения: если t ≠ 0 и t·q = 0, то q = 0.

LaTeX

$$$(\forall t \neq 0)(\forall q \in \mathbb{H}(R;c_1,c_2,c_3))\ (t \cdot q = 0 \Rightarrow q = 0).$$$

Lean4

instance [NoZeroDivisors R] : NoZeroSMulDivisors R ℍ[R,c₁,c₂,c₃] :=
  ⟨by
    rintro t ⟨a, b, c, d⟩ h
    rw [or_iff_not_imp_left]
    intro ht
    simpa [QuaternionAlgebra.ext_iff, ht] using h⟩

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