cast_abs — Mathlib

English

Let q ∈ ℚ and K be an ordered field as above. The embedding respects absolute value: the cast of |q| equals the absolute value of the cast: ((|q| : ℚ) : K) = |(q : K)|.

Русский

Пусть q ∈ ℚ и K — упорядоченное поле. Отображение сохраняет модуль: приведение |q| к K равно модулю приведения q к K.

LaTeX

$$$|q|^K = |q^K|$$$

Lean4

@[simp, norm_cast]
theorem cast_abs (q : ℚ) : ((|q| : ℚ) : K) = |(q : K)| := by simp [abs_eq_max_neg]

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