abs_cast

Mathlib.Data.Nat.Cast.Order.Ring

URI: https://scilib.ai/kg/mathlib#Nat.abs_cast

English

In a ring with order, for natural numbers m,n, (-m : R) = n iff m = 0 and n = 0.

Русский

В кольце с порядком, для натуральных чисел m,n верно, что (-m : R) = n тогда и только тогда, когда m = 0 и n = 0.

LaTeX

$$$(-m : R) = n \iff m = 0 \land n = 0$$$

Lean4

@[simp, norm_cast]
theorem abs_cast (n : ℕ) : |(n : R)| = n :=
  abs_of_nonneg n.cast_nonneg

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

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

Разделы

Аффилиация

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