coe_add_period

Mathlib.Topology.Instances.AddCircle.Defs

URI: https://scilib.ai/kg/mathlib#AddCircle.coe_add_period

English

The period p becomes the identity element in AddCircle p: p maps to 0.

Русский

Период p становится единицей в AddCircle p: образ p равен 0.

LaTeX

$$$$ (p : AddCircle\ p) = 0 $$$$

Lean4

theorem coe_add_period (x : 𝕜) : ((x + p : 𝕜) : AddCircle p) = x := by
  rw [coe_add, ← eq_sub_iff_add_eq', sub_self, coe_period]

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

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

Разделы

Аффилиация

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