Dedekind's modular law for subgroups

The lattice of subgroups of a group is not modular in general, but the modular identity (K ⊓ H) ⊔ N = K ⊓ (H ⊔ N) does hold for N ≤ K as soon as H normalizes N, because then the join H ⊔ N is the product set H * N and the identity is Dedekind's law for products of subgroups (Mathlib's Subgroup.inf_mul_assoc). This is the form in which a kernel is cut out by a normal subgroup it contains together with a complementary subgroup.

Main results

• Subgroup.inf_sup_assoc_of_le: (K ⊓ H) ⊔ N = K ⊓ (H ⊔ N) for H ≤ normalizer N and N ≤ K.

theorem Subgroup.inf_sup_assoc_of_le {G : Type u_1} [Group G] {H K N : Subgroup G} (hHN : H ≤ normalizer ↑N) (h : N ≤ K) : K ⊓ H ⊔ N = K ⊓ (H ⊔ N)

Dedekind's modular law: if H normalizes N and N ≤ K, then (K ⊓ H) ⊔ N = K ⊓ (H ⊔ N).

theorem AddSubgroup.inf_sup_assoc_of_le {G : Type u_1} [AddGroup G] {H K N : AddSubgroup G} (hHN : H ≤ normalizer ↑N) (h : N ≤ K) : K ⊓ H ⊔ N = K ⊓ (H ⊔ N)

Dedekind's modular law: if H normalizes N and N ≤ K, then (K ⊓ H) ⊔ N = K ⊓ (H ⊔ N).