Commit 2025-03-01 21:46 32537238

View on Github →

refactor(Algebra/Group/Subgroup): rename Subgroup.smul_normal to Subgroup.Normal.conj_smul_eq_self (#22291) Rename Subgroup.smul_normal to Subgroup.Normal.conj_smul_eq_self. The result was misnamed, and this PR fixes it with a more descriptive name more in line with the rest of the file.

Estimated changes

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

added theorem Subgroup.Normal.conj_smul_eq_self

deleted theorem Subgroup.smul_normal