rat_mul_iff — Mathlib

English

The product r · x with r ∈ ℚ and r ≠ 0 preserves LiouvilleWith p with the same exponent.

Русский

Произведение r · x с r ∈ ℚ и r ≠ 0 сохраняет LiouvilleWith p с тем же экспонентом.

LaTeX

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

Lean4

/-- The product `r * x`, `r : ℚ`, `r ≠ 0`, is a Liouville number with exponent `p` if and only if
`x` satisfies the same condition. -/
theorem rat_mul_iff (hr : r ≠ 0) : LiouvilleWith p (r * x) ↔ LiouvilleWith p x := by rw [mul_comm, mul_rat_iff hr]

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