rat_sub

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

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

English

If h is LiouvilleWith p x, then LiouvilleWith p (r - x) holds for rational r.

Русский

Если h имеет LiouvilleWith p x, то LiouvilleWith p (r - x) для рационального r.

LaTeX

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

Lean4

theorem rat_sub (h : LiouvilleWith p x) (r : ℚ) : LiouvilleWith p (r - x) :=
  rat_sub_iff.2 h

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

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

Разделы

Аффилиация

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