normEDS_four

Mathlib.NumberTheory.EllipticDivisibilitySequence

URI: https://scilib.ai/kg/mathlib#normEDS_four

English

For every commutative ring R and b, c, d in R, the fourth value of normEDS equals d times b.

Русский

Пусть R — коммутативное кольцо и b, c, d ∈ R. Тогда normEDS(b, c, d, 4) = d · b.

LaTeX

$$$\operatorname{normEDS}(b,c,d,4) = d \cdot b$$$

Lean4

@[simp]
theorem normEDS_four : normEDS b c d 4 = d * b := by simp [normEDS, show ¬Odd (4 : ℤ) by decide]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru