norm_zero

Mathlib.RingTheory.Norm.Basic

URI: https://scilib.ai/kg/mathlib#Algebra.norm_zero

← MathLib Explorer

English

The norm of the zero element in a suitable finite free module is zero.

Русский

Норма нуля в подходящем конечномерном свободном модуле равна нулю.

LaTeX

$$norm R (0 : S) = 0$$

Lean4

@[simp]
theorem norm_zero [Nontrivial S] [Module.Free R S] [Module.Finite R S] : norm R (0 : S) = 0 :=
  by
  nontriviality
  rw [norm_apply, coe_lmul_eq_mul, map_zero, LinearMap.det_zero' (Module.Free.chooseBasis R S)]

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

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

Разделы

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

Аффилиация

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