apply_one

Mathlib.Analysis.Normed.Unbundled.RingSeminorm

URI: https://scilib.ai/kg/mathlib#RingNorm.apply_one

English

For RingNorm R, the unit element acts by (1 : RingNorm R) x = 0 if x = 0, else 1.

Русский

Для RingNorm R единичный элемент действует так: (1 : RingNorm R) x = 0, если x = 0; иначе = 1.

LaTeX

$$$ (1 : RingNorm R)\, x = \begin{cases}0,& x=0\\ 1,& x\neq 0\end{cases} $$$

Lean4

@[simp]
theorem apply_one [DecidableEq R] (x : R) : (1 : RingNorm R) x = if x = 0 then 0 else 1 :=
  rfl

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

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

Разделы

Аффилиация

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