mul_nat

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

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

English

If h is LiouvilleWith p x, then LiouvilleWith p (n · x) for any natural n ≠ 0.

Русский

Если h — LiouvilleWith p x, то LiouvilleWith p (n · x) для любого натурального n ≠ 0.

LaTeX

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

Lean4

theorem mul_nat (h : LiouvilleWith p x) (hn : n ≠ 0) : LiouvilleWith p (x * n) :=
  (mul_nat_iff hn).2 h

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

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

Разделы

Аффилиация

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