Commit 2025-01-06 23:14 d4a7b67c

View on Github →

chore: to_additive various results on groups, group actions (#20498)

Estimated changes

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

Modified Mathlib/GroupTheory/GroupAction/Blocks.lean

added theorem AddAction.IsBlock.of_addsubgroup_of_conjugate

added theorem AddAction.IsBlock.translate

Modified Mathlib/GroupTheory/GroupAction/Pointwise.lean

Modified Mathlib/GroupTheory/GroupAction/SubMulAction.lean

added structure SubAddAction

Modified Mathlib/GroupTheory/Index.lean

modified theorem MulAction.index_stabilizer

modified theorem MulAction.index_stabilizer_of_transitive