one_apply_def

Mathlib.RingTheory.Valuation.Basic

URI: https://scilib.ai/kg/mathlib#Valuation.one_apply_def

English

The one valuation acts by mapping any x to 1 if x ≠ 0 and to 0 if x = 0.

Русский

Единичная оценка отображает любой ненулевой элемент в 1, ноль — в 0.

LaTeX

$$$\\text{one_apply_def}(x) : (1 : Valuation R Γ_0) x = if\\ x=0\\ then\\ 0\\ else\\ 1$$$

Lean4

theorem one_apply_def (x : R) : (1 : Valuation R Γ₀) x = if x = 0 then 0 else 1 :=
  rfl

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

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

Разделы

Аффилиация

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