normEDS_dvd_normEDS_two_mul — Mathlib

English

For all R and b, c, d ∈ R, and any k ∈ ℤ, normEDS(b,c,d,k) divides normEDS(b,c,d,2k).

Русский

Для любых кольца R и элементов b, c, d ∈ R, и любого целого k, выполняется делимость: normEDS(b,c,d,k) делит normEDS(b,c,d,2k).

LaTeX

$$$\operatorname{normEDS}(b,c,d,k) \mid \operatorname{normEDS}(b,c,d,2k)$$$

Lean4

theorem normEDS_dvd_normEDS_two_mul (k : ℤ) : normEDS b c d k ∣ normEDS b c d (2 * k) :=
  ⟨complEDS₂ .., (normEDS_mul_complEDS₂ ..).symm⟩

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