Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.comap_normalizer_eq_of_injective_of_le_range

Modification history

2022-01-26 13:30
src/group_theory/subgroup/basic.lean
feat(group_theory/subgroup/basic): add lemmas related to map, comap, normalizer (#11637) …
Added subgroup.comap_normalizer_eq_of_injective_of_le_rangeView on Github →