instIsCoatomicSubmodule — Mathlib

English

If M is a finite R-module, then the lattice of submodules of M is coatomic.

Русский

Если модуль M над R конечно порожден, то решетка его подмодулей коатомная.

LaTeX

$$Module.Finite.instIsCoatomicSubmodule$$

Lean4

instance [Module.Finite R M] : IsCoatomic (Submodule R M) :=
  CompleteLattice.coatomic_of_top_compact <| by
    rwa [← fg_iff_compact, ← finite_def]
      -- See note [lower instance priority]

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