trivial_apply

Mathlib.Algebra.Order.AbsoluteValue.Basic

URI: https://scilib.ai/kg/mathlib#AbsoluteValue.trivial_apply

English

If x ≠ 0, then the trivial absolute value gives 1: trivial(x) = 1.

Русский

Если x ≠ 0, то тривиальное модульное отображение даёт 1.

LaTeX

$$$x \\neq 0 \\Rightarrow \\operatorname{AbsoluteValue.trivial}(x) = 1$$$

Lean4

@[simp]
theorem trivial_apply {x : R} (hx : x ≠ 0) : AbsoluteValue.trivial (S := S) x = 1 :=
  if_neg hx

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

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

Разделы

Аффилиация

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