normEDS_three

Mathlib.NumberTheory.EllipticDivisibilitySequence

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem normEDS_three : normEDS b c d 3 = c := by simp [normEDS, show ¬Even (3 : ℤ) by decide]

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

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

Разделы

Аффилиация

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