coe_fract

Mathlib.Topology.Instances.AddCircle.Defs

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

English

For any n > 0, the order of the point (p/n) in AddCircle(p) is exactly n.

Русский

Для любого n>0 порядок точки (p/n) в AddCircle(p) равен n.

LaTeX

$$\mathrm{addOrderOf}\left(\left(\tfrac{p}{n}\right) : \mathrm{AddCircle}(p)\right) = n$$

Lean4

@[simp]
theorem coe_fract (x : 𝕜) : (↑(Int.fract x) : AddCircle (1 : 𝕜)) = x := by simp [← Int.self_sub_floor]

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

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

Разделы

Аффилиация

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