sub_rat

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

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

English

@[simp] LiouvilleWith p (x − m) is equivalent to LiouvilleWith p x for any integer m.

Русский

@[simp] LiouvilleWith p (x − m) эквивалентно LiouvilleWith p x для любого целого m.

LaTeX

$$@[simp] theorem sub_int_iff : LiouvilleWith p (x - m) ↔ LiouvilleWith p x$$

Lean4

theorem sub_rat (h : LiouvilleWith p x) (r : ℚ) : LiouvilleWith p (x - r) :=
  sub_rat_iff.2 h

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

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

Разделы

Аффилиация

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