house_intCast — Mathlib

English

If x is an integer, then the house of x (viewed in K) equals its absolute value.

Русский

Если x — целое число, то house(x) равен |x|, когда x трактуется как элемент K.

LaTeX

$$$\\operatorname{house}(x) = |x|$ for $x \\in \\mathbb{Z} \\hookrightarrow K$$$

Lean4

@[simp]
theorem house_intCast (x : ℤ) : house (x : K) = |x| := by
  simp only [house, map_intCast, Pi.intCast_def, pi_norm_const, Complex.norm_intCast, Int.cast_abs]

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