rat_add

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

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

English

If LiouvilleWith p x holds, then LiouvilleWith p (r + x) holds for any rational r.

Русский

Если выполняется LiouvilleWith p x, то для любого рационального r выполняется LiouvilleWith p (r + x).

LaTeX

$$$LiouvilleWith(p, x) \to LiouvilleWith(p, x + r.cast)$$$

Lean4

theorem rat_add (h : LiouvilleWith p x) (r : ℚ) : LiouvilleWith p (r + x) :=
  add_comm x r ▸ h.add_rat r

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

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

Разделы

Аффилиация

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