norm_eq_one_of_not_module_finite — Mathlib

English

If there is no finite generating set (no finite basis) of the S-module over R, then the norm is identically 1 for each x in S.

Русский

Если не существует конечного базиса модуля S над R, норма на любом элементе S равна 1.

LaTeX

$$$ \\text{If } \\text{Module.Finite } R S \\text{ is false, then } \\operatorname{norm} \\, R = 1.$$$

Lean4

theorem norm_eq_one_of_not_module_finite (h : ¬Module.Finite R S) (x : S) : norm R x = 1 :=
  by
  refine norm_eq_one_of_not_exists_basis _ (mt ?_ h) _
  rintro ⟨s, ⟨b⟩⟩
  exact Module.Finite.of_basis b

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