Commit 2024-12-20 09:05 d70be405
View on Github →refactor(Algebra/Group/Subgroup/Basic): Rename normalizer_eq_top to normalizer_eq_top_iff (#20109)
I found myself writing normalizer_eq_top.mpr h a lot when deducing H.normalizer = ⊤ from [h : H.Normal]. Now this becomes H.normalizer_eq_top, and the original iff version of the lemma has been renamed to normalizer_eq_top_iff.