int_mul_iff

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

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

English

For m ∈ ℤ, m ≠ 0, LiouvilleWith p (m · x) holds iff LiouvilleWith p x holds.

Русский

Для m ∈ ℤ, m ≠ 0, LiouvilleWith p (m · x) эквивалентно LiouvilleWith p x.

LaTeX

$$$ LiouvilleWith p (m \cdot x) \iff LiouvilleWith p x $$$

Lean4

theorem int_mul_iff (hm : m ≠ 0) : LiouvilleWith p (m * x) ↔ LiouvilleWith p x := by rw [mul_comm, mul_int_iff hm]

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

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

Разделы

Аффилиация

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