coe_equivIco_mk_apply

Mathlib.Topology.Instances.AddCircle.Defs

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

English

The map equivIco(p,0) sends the quotient class of x to Int.fract(x/p)·p in AddCircle(p).

Русский

Карта equivIco(p,0) отправляет класс x/ p в AddCircle(p) в виде Int.fract(x/p)·p.

LaTeX

$$$(equivIco(p,0))(x) = \operatorname{Int.fract}(x/p)\cdot p$ in AddCircle(p)$$

Lean4

@[simp]
theorem coe_equivIco_mk_apply (x : 𝕜) : (equivIco p 0 <| QuotientAddGroup.mk x : 𝕜) = Int.fract (x / p) * p :=
  toIcoMod_eq_fract_mul _ x

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

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

Разделы

Аффилиация

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