int_add_iff

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

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

English

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

Русский

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

LaTeX

$$$LiouvilleWith(p, x + m) \iff LiouvilleWith(p, x)$$$

Lean4

@[simp]
theorem int_add_iff : LiouvilleWith p (m + x) ↔ LiouvilleWith p x := by rw [add_comm, add_int_iff]

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

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

Разделы

Аффилиация

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