mul_int

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

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

English

If h is LiouvilleWith p x and m ≠ 0 is an integer, then LiouvilleWith p (m · x) holds.

Русский

Если h — LiouvilleWith p x и m ≠ 0, целое, то LiouvilleWith p (m · x) выполняется.

LaTeX

$$$ \forall p\ x\in \mathbb R,\ \forall m \in \mathbb Z,\ m \neq 0\Rightarrow LiouvilleWith p (m \cdot x) $$$

Lean4

theorem mul_int (h : LiouvilleWith p x) (hm : m ≠ 0) : LiouvilleWith p (x * m) :=
  (mul_int_iff hm).2 h

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

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

Разделы

Аффилиация

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