Theorem AddSubgroup.inertia_top

Modification history

2026-09-26 10:13
Mathlib/Algebra/Group/Subgroup/Basic.lean
feat(RingTheory/Ideal): the `⊥` and `⊤` cases of the pointwise action on ideals (#44070) …
Added AddSubgroup.inertia_topView on Github →