int_sub_iff

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

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

English

LiouvilleWith p (m - x) is equivalent to LiouvilleWith p x for integer m.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem int_sub_iff : LiouvilleWith p (m - x) ↔ LiouvilleWith p x := by simp [sub_eq_add_neg]

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

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

Разделы

Аффилиация

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