toIcoDiv_eq_of_sub_zsmul_mem_Ico

Mathlib.Algebra.Order.ToIntervalMod

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

← MathLib Explorer

English

If b − n·p ∈ [a, a+p), then toIcoDiv hp a b = n.

Русский

Если b − n·p ∈ [a, a+p), то toIcoDiv hp a b = n.

LaTeX

$$$ b - n p \in [a, a+p) \Rightarrow \mathrm{toIcoDiv}(hp,a,b) = n $$$

Lean4

theorem toIcoDiv_eq_of_sub_zsmul_mem_Ico (h : b - n • p ∈ Set.Ico a (a + p)) : toIcoDiv hp a b = n :=
  ((existsUnique_sub_zsmul_mem_Ico hp b a).choose_spec.2 _ h).symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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