nat_mul

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

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

English

If h is LiouvilleWith p x and n ≠ 0, then LiouvilleWith p (n · x).

Русский

Если h — LiouvilleWith p x и n ≠ 0, то LiouvilleWith p (n · x).

LaTeX

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

Lean4

theorem nat_mul (h : LiouvilleWith p x) (hn : n ≠ 0) : LiouvilleWith p (n * x) := by rw [mul_comm]; exact h.mul_nat hn

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

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

Разделы

Аффилиация

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