normEDS_one

Mathlib.NumberTheory.EllipticDivisibilitySequence

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

English

For all b,c,d in a commutative ring, normEDS(b,c,d,1) = 1.

Русский

Для любых b,c,d в коммутативном кольце выполняется normEDS(b,c,d,1) = 1.

LaTeX

$$$$\text{normEDS}(b,c,d,1) = 1.$$$$

Lean4

@[simp]
theorem normEDS_one : normEDS b c d 1 = 1 := by simp [normEDS]

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

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

Разделы

Аффилиация

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