Commit 2025-11-24 11:02 0cfb85e9

View on Github →

feat(Algebra/Group/Subgroup/Basic): API lemma relating inertia and subgroupOf (#31572) This PR adds an API lemma relating inertia and subgroupOf.

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/Basic.lean

added theorem AddSubgroup.inertia_map_subtype

added theorem AddSubgroup.subgroupOf_inertia

Modified Mathlib/RingTheory/Ideal/Over.lean