k-transitivity and primitivity of an action

Stream: Is there code for X?

[Edward van de Meent]

given some instance of SMul G M, G acts k-transitively on M (and the action of G on M is k-transitive) when every function defined on k elements of M is the restriction of the action of (g:G) on M

given some instance of SMul G M, G acts primitively on M (and the action of G on M is primitive) when given some partition of M (dictated by an equivalence relation R) such that the action of every (g:G) keeps the partition intact, that partition is either top or bottom (i.e. either you have a single subset containing all elements of M, or you have a singleton for every element)

is there code for this? i couldn't find it.

[Anatole Dedecker]

@Antoine Chambert-Loir Did you define this as part of your work on permutation groups ?

[Antoine Chambert-Loir]

Yes ! but it's not in mathlib yet. (To be in mathlib, I need to have branch#SMulSemiHom merged…)
However, it can be accessed at https://github.com/AntoineChambert-Loir/Jordan4/tree/main/Jordan

Multiple transitivity is at https://github.com/AntoineChambert-Loir/Jordan4/blob/735924420678d50f4618b8c11057fe1c3b9d50be/Jordan/MultipleTransitivity.lean#L115

Primitivity is at https://github.com/AntoineChambert-Loir/Jordan4/blob/735924420678d50f4618b8c11057fe1c3b9d50be/Jordan/Primitive.lean#L112

[Edward van de Meent]

in case someone else is searching for the same thing: 1-transitivity is already defined, see here in the docs