nat_mul_iff

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

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

English

For n ≠ 0, LiouvilleWith p (n · x) ↔ LiouvilleWith p x.

Русский

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

LaTeX

$$$ \forall {p x : \mathbb R} {n : \mathbb N}, n \neq 0 \Rightarrow LiouvilleWith p (n \cdot x) \iff LiouvilleWith p x $$$

Lean4

theorem nat_mul_iff (hn : n ≠ 0) : LiouvilleWith p (n * x) ↔ LiouvilleWith p x := by rw [mul_comm, mul_nat_iff hn]

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

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

Разделы

Аффилиация

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