complEDS₂_four — Mathlib

English

For all b,c,d, complEDS₂(b,c,d,4) = c^2 · preNormEDS(b^4) c d 6 − [preNormEDS(b^4) c d 5]^2.

Русский

Для любых b,c,d выполняется complEDS₂(b,c,d,4) = c^2 · preNormEDS(b^4) c d 6 − [preNormEDS(b^4) c d 5]^2.

LaTeX

$$$$\text{complEDS}_2(b,c,d,4) = c^2 \cdot \text{preNormEDS}(b^4) c d 6 - \big( \text{preNormEDS}(b^4) c d 5 \big)^2.$$$$

Lean4

@[simp]
theorem complEDS₂_four : complEDS₂ b c d 4 = c ^ 2 * preNormEDS (b ^ 4) c d 6 - preNormEDS (b ^ 4) c d 5 ^ 2 := by
  simp [complEDS₂, if_pos (by decide : Even (4 : ℤ))]

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