Commit 2025-02-04 20:48 3f98c55d

View on Github →

feat: primitive group actions (#12052) This PR defines the notion of a primitive action. This concept is used to state the Iwasawa criterion for simplicity of #12048

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

added theorem MulAction.fixedPoints_of_subsingleton

added theorem MulAction.nontrivial_of_fixedPoints_ne_univ

added theorem MulAction.subsingleton_orbit_iff_mem_fixedPoints

Modified Mathlib/GroupTheory/GroupAction/Blocks.lean

Created Mathlib/GroupTheory/GroupAction/Primitive.lean

added theorem MulAction.IsBlock.subsingleton_or_eq_univ

added theorem MulAction.IsPreprimitive.isCoatom_stabilizer_of_isPreprimitive

added theorem MulAction.IsPreprimitive.of_isTrivialBlock_base

added theorem MulAction.IsPreprimitive.of_isTrivialBlock_of_not_mem_fixedPoints

added theorem MulAction.IsPreprimitive.of_subsingleton

added theorem MulAction.IsPreprimitive.of_surjective

added theorem MulAction.isCoatom_stabilizer_iff_preprimitive

added theorem MulAction.isPreprimitive_congr

added theorem MulAction.isSimpleOrder_blockMem_iff_isPreprimitive

added theorem MulAction.mk'

Modified Mathlib/GroupTheory/GroupAction/Transitive.lean

deleted theorem MulAction.isPretransitive_iff_orbit_eq_top

added theorem MulAction.isPretransitive_iff_orbit_eq_univ