normEDS_two

Mathlib.NumberTheory.EllipticDivisibilitySequence

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem normEDS_two : normEDS b c d 2 = b := by simp [normEDS]

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

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

Разделы

Аффилиация

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