add_nat

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

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

English

If h is LiouvilleWith p x, then LiouvilleWith p (x + n) holds for any natural n.

Русский

Если h является LiouvilleWith p x, то LiouvilleWith p (x + n) верно для любого натурального n.

LaTeX

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

Lean4

theorem add_nat (h : LiouvilleWith p x) (n : ℕ) : LiouvilleWith p (x + n) :=
  h.add_int n

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

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

Разделы

Аффилиация

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