preNormEDS' — Mathlib

English

For any a,b in α with a=0 ↔ b=0, the product a·b lies in {0,1,2,3,4} if and only if (a,b) lies in the explicit 17-element set of pairs (as given in the statement).

Русский

Для любых a,b в α с a=0 ⇔ b=0 произведение a·b принадлежит {0,1,2,3,4} тогда и только тогда, когда пара (a,b) принадлежит перечисленному явному множеству из 17 пар.

LaTeX

$$$ a,b : α,\ (a=0 \iff b=0) \Rightarrow a b \in \{0,1,2,3,4\} \iff (a,b) \in \{(0,0),(1,1),(-1,-1),(1,2),(2,1),(-1,-2),(-2,-1),(1,3),(3,1),(-1,-3),(-3,-1),(4,1),(1,4),(-4,-1),(-1,-4),(2,2),(-2,-2)\}$$$

Lean4

/-- The auxiliary sequence for a normalised EDS `W : ℕ → R`, with initial values
`W(0) = 0`, `W(1) = 1`, `W(2) = 1`, `W(3) = c`, and `W(4) = d` and extra parameter `b`. -/
def preNormEDS' : ℕ → R
  | 0 => 0
  | 1 => 1
  | 2 => 1
  | 3 => c
  | 4 => d
  | (n + 5) =>
    let m := n / 2
    if hn : Even n then
      preNormEDS' (m + 4) * preNormEDS' (m + 2) ^ 3 * (if Even m then b else 1) -
        preNormEDS' (m + 1) * preNormEDS' (m + 3) ^ 3 * (if Even m then 1 else b)
    else
      have : m + 5 < n + 5 := add_lt_add_right (Nat.div_lt_self (Nat.not_even_iff_odd.mp hn).pos one_lt_two) 5
      preNormEDS' (m + 2) ^ 2 * preNormEDS' (m + 3) * preNormEDS' (m + 5) -
        preNormEDS' (m + 1) * preNormEDS' (m + 3) * preNormEDS' (m + 4) ^ 2

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