instInhabitedAlgebraNorm

Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

URI: https://scilib.ai/kg/mathlib#instInhabitedAlgebraNorm

Lean4

instance (K : Type*) [NormedField K] : Inhabited (AlgebraNorm K K) :=
  ⟨{  toFun := norm
      map_zero' := norm_zero
      add_le' := norm_add_le
      neg' := norm_neg
      smul' := norm_mul
      mul_le' := norm_mul_le
      eq_zero_of_map_eq_zero' := fun _ => norm_eq_zero.mp }⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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