map_units_int_smul — Mathlib

English

Absolute value is invariant under multiplication by a unit of integers on the left.

Русский

Абсолютная величина не изменяется при умножении слева на единицы целых.

LaTeX

$$$$ \\operatorname{abv}(x \\cdot y) = \\operatorname{abv}(y) $$$$

Lean4

@[simp]
theorem map_units_int_smul (abv : AbsoluteValue R S) (x : ℤˣ) (y : R) : abv (x • y) = abv y := by
  rcases Int.units_eq_one_or x with (rfl | rfl) <;> simp

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