8.3. The left multiplication action on subsets🔗

A group acts on its subsets by left multiplication. Recall that given a group structure Group G on a type G, the type of subsets of G is Set G. Mathlib provides an instance Set.mulActionSet : MulAction G (Set G) for this action, and notation g • S for the action of g : G on S : Set G, which is enabled in the Pointwise namespace.

open scoped Pointwise
open DihedralGroup

def S : Set (DihedralGroup 3) := {.r 0, .r 1}
def g : DihedralGroup 3 := .r 0
example : g • S = {.r 0, .r 1} := byG:Type u_1X:Type u_2inst✝¹:Monoid Gx:Xinst✝:MulAction G X⊢ g • S = {r 0, r 1}
  simp [g, S]All goals completed! 🐙