val_zsmul — Mathlib

English

For integer scaling, the valuation commutes with zsmul: (n • y).val = n • y.val for all n ∈ ℤ and y ∈ HomogeneousLocalization 𝒜 x.

Русский

Для целочисленного масштабирования верно: (n • y).val = n • y.val для всех n ∈ ℤ и y ∈ HomogeneousLocalization 𝒜 x.

LaTeX

$$$\mathrm{val}(n\cdot y) = n\cdot\mathrm{val}(y)$$$

Lean4

theorem val_zsmul (n : ℤ) (y : HomogeneousLocalization 𝒜 x) : (n • y).val = n • y.val := by
  rw [val_smul, OreLocalization.zsmul_eq_zsmul]

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