finite_sup — Mathlib

English

If M is finite over R, then Mᵐᵒᵖ is finite over R.

Русский

Если M конечен как R-модуль, то Mᵐᵒᵖ также конечен над R.

LaTeX

$$$\\forall R\\, M\\; [\\text{Module.Finite } R M] \\Rightarrow \\text{Module.Finite } R (M^{\\text{op}})$$$

Lean4

/-- The sup of two fg submodules is finite. Also see `Submodule.FG.sup`. -/
instance finite_sup (S₁ S₂ : Submodule R V) [h₁ : Module.Finite R S₁] [h₂ : Module.Finite R S₂] :
    Module.Finite R (S₁ ⊔ S₂ : Submodule R V) := by
  rw [finite_def] at *
  exact (fg_top _).2 (((fg_top S₁).1 h₁).sup ((fg_top S₂).1 h₂))

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