normSq_eq_zero — Mathlib

English

normSq(a) = 0 if and only if a = 0, for quaternions a over a ordered ring.

Русский

normSq(a) = 0 тогда и только тогда, когда a = 0, для квартонионов над упорядоченным кольцом.

LaTeX

$$normSq(a) = 0 \iff a = 0$$

Lean4

@[simp]
theorem normSq_eq_zero : normSq a = 0 ↔ a = 0 :=
  by
  refine ⟨fun h => ?_, fun h => h.symm ▸ normSq.map_zero⟩
  rw [normSq_def', add_eq_zero_iff_of_nonneg, add_eq_zero_iff_of_nonneg, add_eq_zero_iff_of_nonneg] at h
  · exact ext a 0 (pow_eq_zero h.1.1.1) (pow_eq_zero h.1.1.2) (pow_eq_zero h.1.2) (pow_eq_zero h.2)
  all_goals apply_rules [sq_nonneg, add_nonneg]

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