Commit 2024-10-04 10:12 8834646c

View on Github →

feat(Topology/Group): Open normal subgroup (#16980) Define the type of open normal subgroup in a topological group.

Estimated changes

Modified Mathlib/Topology/Algebra/OpenSubgroup.lean

added structure OpenNormalAddSubgroup

added theorem OpenNormalSubgroup.toSubgroup_injective

added structure OpenNormalSubgroup