add_int

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

URI: https://scilib.ai/kg/mathlib#LiouvilleWith.add_int

English

If h is LiouvilleWith p x, then for any integer m, LiouvilleWith p (x + m) holds.

Русский

Если h имеет свойство LiouvilleWith p x, то для любого целого m верно LiouvilleWith p (x + m).

LaTeX

$$$LiouvilleWith(p, x) \to LiouvilleWith(p, x + m)$$$

Lean4

theorem add_int (h : LiouvilleWith p x) (m : ℤ) : LiouvilleWith p (x + m) :=
  add_int_iff.2 h

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

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

Разделы

Аффилиация

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