mul_rat_iff — Mathlib

English

The product of a Liouville number by a nonzero rational is again Liouville with the same exponent.

Русский

Произведение числа Лиувиля на ненулевой рационал снова число Лиувиля с тем же экспонентом.

LaTeX

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

Lean4

/-- The product `x * r`, `r : ℚ`, `r ≠ 0`, is a Liouville number with exponent `p` if and only if
`x` satisfies the same condition. -/
theorem mul_rat_iff (hr : r ≠ 0) : LiouvilleWith p (x * r) ↔ LiouvilleWith p x :=
  ⟨fun h => by
    simpa only [mul_assoc, ← Rat.cast_mul, mul_inv_cancel₀ hr, Rat.cast_one, mul_one] using h.mul_rat (inv_ne_zero hr),
    fun h => h.mul_rat hr⟩

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