preNormEDS_mul_complEDS₂ — Mathlib

English

For all integers k, preNormEDS(b^4) c d k · complEDS₂(b,c,d) k = preNormEDS(b^4) c d (2k) · (if Even k then 1 else b).

Русский

Для всех целых k выполняется произведение preNormEDS(b^4) c d k на complEDS₂(b,c,d) k равняется preNormEDS(b^4) c d (2k) умноженному на (если k чётное, тогда 1, иначе b).

LaTeX

$$$$\text{preNormEDS}(b^4) c d k \cdot \text{complEDS}_2(b,c,d) k = \text{preNormEDS}(b^4) c d (2k) \cdot \big(\text{Even } k \ ? \ 1 \ : \ b\big).$$$$

Lean4

theorem preNormEDS_mul_complEDS₂ (k : ℤ) :
    preNormEDS (b ^ 4) c d k * complEDS₂ b c d k = preNormEDS (b ^ 4) c d (2 * k) * if Even k then 1 else b :=
  by
  rw [complEDS₂, preNormEDS_even]
  ring1

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