norm_ne_zero_iff_of_basis

Mathlib.RingTheory.Norm.Basic

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

← MathLib Explorer

English

In a domain setting with a basis, the nonzero norm of x is equivalent to x ≠ 0.

Русский

Для области и базиса: нормa x не равна нулю эквивалентна x ≠ 0.

LaTeX

$$norm_ne_zero_iff_of_basis (b) {x} : Algebra.norm R x ≠ 0 ↔ x ≠ 0$$

Lean4

theorem norm_ne_zero_iff_of_basis [IsDomain R] [IsDomain S] (b : Basis ι R S) {x : S} : Algebra.norm R x ≠ 0 ↔ x ≠ 0 :=
  not_iff_not.mpr (norm_eq_zero_iff_of_basis b)

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

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

Разделы

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

Аффилиация

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