lean_workbook_plus_17203

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let $H_1, H_2$ be two normal subgroups of $G$ . Show that $H_1\cap H_2$ is normal.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17203 {G : Type*} [Group G] {H1 H2 : Subgroup G}
  (h1 : H1.Normal) (h2 : H2.Normal) : (H1 ⊓ H2).Normal   :=  by sorry

Source