Commit 2025-05-14 09:23 bdbaaec4

View on Github →

feat(GroupTheory/GroupAction/Basic): equivalences between stabilizers (#24107) Define equivalence between stabilizers.

Estimated changes

Modified Mathlib/Algebra/Group/End.lean

modified theorem Equiv.Perm.MulAut.symm_inv

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

added def AddAction.stabilizerEquivStabilizer

added theorem AddAction.stabilizerEquivStabilizer_apply

added theorem AddAction.stabilizerEquivStabilizer_neg

added theorem AddAction.stabilizerEquivStabilizer_symm

added theorem AddAction.stabilizerEquivStabilizer_symm_apply

added theorem AddAction.stabilizerEquivStabilizer_trans

added theorem AddAction.stabilizerEquivStabilizer_zero

added def MulAction.stabilizerEquivStabilizer

added theorem MulAction.stabilizerEquivStabilizer_apply

added theorem MulAction.stabilizerEquivStabilizer_inv

added theorem MulAction.stabilizerEquivStabilizer_one

added theorem MulAction.stabilizerEquivStabilizer_symm

added theorem MulAction.stabilizerEquivStabilizer_symm_apply

added theorem MulAction.stabilizerEquivStabilizer_trans