norm_eq_zero_iff_of_basis — Mathlib

English

A variant of the previous statement, using a general basis, yields the same zero-norm equivalence.

Русский

Вариант предыдущего утверждения для общего базиса даёт ту же эквивалентность нулевой нормы.

LaTeX

$$norm_eq_zero_iff_of_basis (b) {x} : algebra.norm R x = 0 ↔ x = 0$$

Lean4

theorem norm_eq_zero_iff_of_basis [IsDomain R] [IsDomain S] (b : Basis ι R S) {x : S} : Algebra.norm R x = 0 ↔ x = 0 :=
  by
  haveI : Module.Free R S := Module.Free.of_basis b
  haveI : Module.Finite R S := Module.Finite.of_basis b
  exact norm_eq_zero_iff

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