nat_add_iff

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

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

English

For all p, x real and n natural, LiouvilleWith p (n + x) holds whenever LiouvilleWith p x holds.

Русский

Пусть p, x вещественные, n натуральное. Если LiouvilleWith p x, то LiouvilleWith p (n + x).

LaTeX

$$$LiouvilleWith(p, x) \to LiouvilleWith(p, x + n)$$$

Lean4

@[simp]
theorem nat_add_iff : LiouvilleWith p (n + x) ↔ LiouvilleWith p x := by rw [add_comm, add_nat_iff]

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

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

Разделы

Аффилиация

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