mathlib3

36a35211 - feat(group_theory/group_action/support): Support under an action (#17055)

feat(group_theory/group_action/support): Support under an action (#17055) Given an action of a group `G` on a type `α`, we say that a set `s : set α ` **supports** an element `a : α` if, for all `g`, `g` fixes `a` if `g` fixes `s` pointwise.