free — Mathlib

English

If M is a finitely generated R-submodule of V with hr: rank_K V ≤ rank_R M, then M is a lattice over K.

Русский

Если M является конечно порождённой подмодулей V над R и rank_K V ≤ rank_R M, то M является решёткой над K.

LaTeX

$$$M \text{ FG and } \operatorname{rank}_K V \le \operatorname{rank}_R M \;\Rightarrow\; IsLattice_K M$$$

Lean4

/-- Any lattice over a PID is a free `R`-module.
Note that under our conditions, `NoZeroSMulDivisors R K` simply says that `algebraMap R K` is
injective. -/
instance free [NoZeroSMulDivisors R K] (M : Submodule R V) [IsLattice K M] : Module.Free R M :=
  by
  have := NoZeroSMulDivisors.trans_faithfulSMul R K V
  infer_instance

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