norm_eq_zero_iff' — Mathlib

English

For a basis b, the norm of any x equals zero exactly when x equals zero.

Русский

Для базиса b норма любого x равна 0 тогда и только тогда, когда x = 0.

LaTeX

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

Lean4

/-- This is `Algebra.norm_eq_zero_iff` composed with `Algebra.norm_apply`. -/
@[simp]
theorem norm_eq_zero_iff' [IsDomain R] [IsDomain S] [Module.Free R S] [Module.Finite R S] {x : S} :
    LinearMap.det (LinearMap.mul R S x) = 0 ↔ x = 0 :=
  norm_eq_zero_iff

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