Commit 2026-06-23 12:44 7ff2d88e

View on Github →

feat(RingTheory/Ideal/Defs): add Ideal.coe_mem_inertia (#40383) This PR adds a lemma coe_mem_inertia for the situation when a coercion from a subgroup lies in an inertia subgroup. I added both an AddSubgroup version and an Ideal version to allow for better rewriting.

Estimated changes

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

added theorem AddSubgroup.coe_mem_inertia

modified def AddSubgroup.inertia

modified theorem AddSubgroup.inertia_map_subtype

modified theorem AddSubgroup.mem_inertia

modified theorem AddSubgroup.subgroupOf_inertia

Modified Mathlib/RingTheory/Ideal/Defs.lean

added theorem Ideal.coe_mem_inertia