finite — Mathlib

English

A power basis pb for S over R implies that S is a finite R-module, i.e., Module.Finite R S.

Русский

База PowerBasis pb для S над R даёт, что S — конечномодуль над R, то есть Module.Finite R S.

LaTeX

$$$\\text{PowerBasis}_R S \\ \\Rightarrow \\ \\text{Module.Finite } R S$$$

Lean4

/-- Cannot be an instance because `PowerBasis` cannot be a class. -/
theorem finite (pb : PowerBasis R S) : Module.Finite R S :=
  .of_basis pb.basis

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