Theorem SubMulAction.ofFixingSubgroup_of_inclusion_injective

Modification history

2025-07-07 17:19
Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean
feat(GroupTheory/GroupAction/Jordan) : Primitivity lemmas (#26280) …
Modified SubMulAction.ofFixingSubgroup_of_inclusion_injectiveView on Github →
2025-06-27 03:35
Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean
feat: Multiple Primitivity of group actions (#26279) …
Modified SubMulAction.ofFixingSubgroup_of_inclusion_injectiveView on Github →
2025-06-15 08:42
Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean
feat(GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup): action of the fixing Subgroup on the complement of a set (#23970) …
Added SubMulAction.ofFixingSubgroup_of_inclusion_injectiveView on Github →