finsupp — Mathlib

English

If R → S → M is a scalar tower with M free as an S-module and S free as an R-module (and appropriate commutativity/tower hypotheses), then M is free as an R-module.

Русский

Если имеется каскад скаляров R → S → M и M свободен как модуль над S, а S свободен над R, то M свободен как модуль над R.

LaTeX

$$$\\text{Module.Free } R M$ given $\\text{Module.Free } S M$, $\\text{Module.Free } R S$, and the scalar tower conditions$$

Lean4

instance _root_.Module.Free.finsupp [Module.Free R M] : Module.Free R (ι →₀ M) :=
  .of_basis (Finsupp.basis fun _ => Module.Free.chooseBasis R M)

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