normSq_def' — Mathlib

English

normSq a equals a.1^2 + a.2^2 + a.3^2 + a.4^2, i.e., the sum of squares of its four components.

Русский

normSq a равно a.1^2 + a.2^2 + a.3^2 + a.4^2, то есть сумма квадратов его четырех компонент.

LaTeX

$$$ normSq\ a = a.1^2 + a.2^2 + a.3^2 + a.4^2 $$$

Lean4

theorem normSq_def' : normSq a = a.1 ^ 2 + a.2 ^ 2 + a.3 ^ 2 + a.4 ^ 2 := by
  simp only [normSq_def, sq, mul_neg, sub_neg_eq_add, re_mul, re_star, imI_star, imJ_star, imK_star]

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