cast_abs

Mathlib.Algebra.Order.Ring.Cast

URI: https://scilib.ai/kg/mathlib#Int.cast_abs

English

The cast of the natural absolute value equals the absolute value of the cast: (natAbs n).cast = |n| cast.

Русский

Приведение натуральной абсолютной величины равно абсолютному значению приведения: natAbs(n).cast = |n| cast.

LaTeX

$$n^{\mathsf{natAbs}}^{\mathsf{cast}} = |n|^{\mathsf{cast}}$$

Lean4

@[simp, norm_cast]
theorem cast_abs : (↑|a| : R) = |(a : R)| := by simp [abs_eq_max_neg]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru