apply_one

Mathlib.Analysis.Normed.Unbundled.RingSeminorm

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

English

The unit action for MulRingSeminorm mirrors that of RingSeminorm: (1 : MulRingSeminorm R) x = 0 if x = 0, else 1.

Русский

Единичная дія MulRingSeminorm совпадает с RingSeminorm: (1 : MulRingSeminorm R) x = 0, если x = 0; иначе 1.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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