instIsModularLatticeSubgroup — Mathlib

English

In a commutative group, the collection of all subgroups forms a modular lattice. Equivalently, for any subgroups A, B, C with A ≤ C, the modular law A + (B ∩ C) = (A + B) ∩ C holds.

Русский

В коммутативной группе множество подгрупп образует модульную решётку. Аналогично, при подгруппах A ≤ C выполняется тождество модульного закона: A + (B ∩ C) = (A + B) ∩ C.

LaTeX

$$$A \le C \;\Rightarrow\; A + (B \cap C) = (A + B) \cap C$$$

Lean4

@[to_additive]
instance : IsModularLattice (Subgroup C) :=
  ⟨fun {x} 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]
    exact ⟨b, hb, c, mem_inf.2 ⟨hc, (mul_mem_cancel_left (xz hb)).1 haz⟩, rfl⟩⟩

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