toRingNorm_apply

Mathlib.Analysis.Normed.Unbundled.RingSeminorm

URI: https://scilib.ai/kg/mathlib#NormedRing.toRingNorm_apply

English

The ring norm toRingNorm acts as the usual norm: for any x ∈ R, (toRingNorm R) x = ||x||.

Русский

Кольцевой норме toRingNorm действует как обычная норма: для любого x ∈ R, (toRingNorm R) x = ||x||.

LaTeX

$$$(\text{toRingNorm } R)\,x = \|x\|$$$

Lean4

@[simp]
theorem toRingNorm_apply (R : Type*) [NormedRing R] (x : R) : (NormedRing.toRingNorm R) x = ‖x‖ :=
  rfl

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

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

Разделы

Аффилиация

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