normEDS_mul_complEDS₂ — Mathlib

English

For any commutative ring R and elements b, c, d ∈ R, and any integer k, normEDS(b,c,d,k) multiplied by complEDS₂(b,c,d,k) equals normEDS(b,c,d,2k).

Русский

Пусть R — коммутативное кольцо, а b, c, d ∈ R. Тогда normEDS(b,c,d,k) · complEDS₂(b,c,d,k) = normEDS(b,c,d,2k) для любого целого k.

LaTeX

$$$\operatorname{normEDS}(b,c,d,k) \cdot \operatorname{complEDS}_2(b,c,d,k) = \operatorname{normEDS}(b,c,d,2k)$$$

Lean4

theorem normEDS_mul_complEDS₂ (k : ℤ) : normEDS b c d k * complEDS₂ b c d k = normEDS b c d (2 * k) := by
  simp_rw [normEDS, mul_right_comm, preNormEDS_mul_complEDS₂, mul_assoc, apply_ite₂, one_mul, mul_one, ite_self,
    if_pos <| even_two_mul k]

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