complEDS₂_three — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem complEDS₂_three : complEDS₂ b c d 3 = preNormEDS (b ^ 4) c d 5 * b - d ^ 2 * b := by
  simp [complEDS₂, if_neg (by decide : ¬Even (3 : ℤ)), sub_mul]

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