nnqsmul_mk — Mathlib

English

For a nonnegative rational a = a.num / a.den, a • mk m s = mk (a.num • m) ((a.den, a.den_pos) * s) in the localized setting.

Русский

Для неотрицательного рационального a = a.num / a.den выполняется a • mk m s = mk (a.num • m) ((a.den, a.den_pos) * s) в локализации.

LaTeX

$$$a \;\text{nqsmul} \;\text{mk } m s = \text{mk } (a.num \cdot m) (\langle a.den, a.den_pos \rangle \cdot s)$$$

Lean4

theorem nnqsmul_mk (a : ℚ≥0) (m : M) (s : ℕ+) : a • mk m s = mk (a.num • m) (⟨a.den, a.den_pos⟩ * s) :=
  by
  convert LocalizedModule.mk'_smul_mk ℚ≥0 a.num m ⟨a.den, by simp⟩ (↑ⁿ s)
  simp [IsLocalization.eq_mk'_iff_mul_eq]

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