map_units_intCast — Mathlib

English

The absolute value of the cast of a unit of integers, into any ring R, is 1.

Русский

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

LaTeX

$$$$ \\lvert (x : \\mathbb{Z}) : R \\rvert = 1 \\quad \\text{for } x \\in \\mathbb{Z}^× $$$$

Lean4

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

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