Theorem Subgroup.Normal.conj_smul_eq_self

Modification history

2025-03-01 21:46

Mathlib/Algebra/Group/Subgroup/Pointwise.lean

refactor(Algebra/Group/Subgroup): rename `Subgroup.smul_normal` to `Subgroup.Normal.conj_smul_eq_self` (#22291) …

Added Subgroup.Normal.conj_smul_eq_self View on Github →