sub_rat_iff

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

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

English

LiouvilleWith p (r - x) is equivalent to LiouvilleWith p x for rational r.

Русский

LiouvilleWith p (r - x) эквивалентно LiouvilleWith p x для рационального r.

LaTeX

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

Lean4

@[simp]
theorem sub_rat_iff : LiouvilleWith p (x - r) ↔ LiouvilleWith p x := by rw [sub_eq_add_neg, ← Rat.cast_neg, add_rat_iff]

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

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

Разделы

Аффилиация

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