Commit 2024-11-18 10:08 15fca276

View on Github →

refactor(GroupTheory/Index): Remove unnecessary coercions to Set in index_ker and relindex_ker (#19105) This PR removes unnecessary coercions to Set in index_ker and relindex_ker.

Estimated changes

Modified Mathlib/GroupTheory/Index.lean

modified theorem Subgroup.index_ker

modified theorem Subgroup.relindex_ker