instIsModularLattice — Mathlib

English

The collection of submodules of a module forms a modular lattice.

Русский

Множество подмодулей модуля образует модульную решетку.

LaTeX

$$$\operatorname{IsModularLattice}(\mathrm{Submodule}(R,M))$$$

Lean4

instance : IsModularLattice (Submodule R M) :=
  ⟨fun y z xz a ha => by
    rw [mem_inf, mem_sup] at ha
    rcases ha with ⟨⟨b, hb, c, hc, rfl⟩, haz⟩
    rw [mem_sup]
    refine ⟨b, hb, c, mem_inf.2 ⟨hc, ?_⟩, rfl⟩
    rw [← add_sub_cancel_right c b, add_comm]
    apply z.sub_mem haz (xz hb)⟩

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