normEDS_ofNat — Mathlib

English

For any commutative ring R and b,c,d ∈ R and any natural n, normEDS(b,c,d,n) = preNormEDS′(b^4) c d n · if Even n then b else 1.

Русский

Пусть R — коммутативное кольцо, а b,c,d ∈ R, и пусть n ∈ ℕ. Тогда normEDS(b,c,d,n) = preNormEDS′(b^4) c d n · (если n чётно, то b, иначе 1).

LaTeX

$$$$\text{normEDS}(b,c,d,n) = \text{preNormEDS}'(b^4) c d n \cdot \begin{cases} b, & \text{Even } n \\ 1, & \text{else} \end{cases}.$$$$

Lean4

@[simp]
theorem normEDS_ofNat (n : ℕ) : normEDS b c d n = preNormEDS' (b ^ 4) c d n * if Even n then b else 1 := by
  simp [normEDS]

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