rat_mul — Mathlib

English

If h is LiouvilleWith p x, then h is LiouvilleWith p (r · x) for any nonzero rational r; equivalently, rat_mul preserves LiouvilleWith.

Русский

Если h является LiouvilleWith p x, то оно сохраняется под умножением на ненулевое рациональное r: LiouvilleWith p (r · x).

LaTeX

$$$ \text{(LiouvilleWith RatMul)}:\quad LiouvilleWith p (r \cdot x) \Rightarrow LiouvilleWith p x $$$

Lean4

theorem rat_mul (h : LiouvilleWith p x) (hr : r ≠ 0) : LiouvilleWith p (r * x) :=
  (rat_mul_iff hr).2 h

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