Pointwise fixing subgroups

This file records small generic additions to Mathlib's fixingSubgroup API.

@[simp]

theorem TauCeti.fixingSubgroup_univ {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [FaithfulSMul G α] : fixingSubgroup G Set.univ = ⊥

For a faithful action, the subgroup fixing the whole space pointwise is trivial.