nat_sub_iff

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

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

English

LiouvilleWith p (x - n) is equivalent to LiouvilleWith p x for natural n.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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