Theorems · Definition · group theory

Finset.mulAction

{α : Type u_2} →
  {β : Type u_3} →
    [DecidableEq β] → [inst : DecidableEq α] → [inst_1 : Monoid α] → [MulAction α β] → MulAction (Finset α) (Finset β)

A multiplicative action of a monoid α on a type β gives a multiplicative action of Finset α on Finset β.

Defined in: Mathlib.Algebra.Group.Action.Pointwise.Finset
Cited by: 0 results in Mathlib
Foundations: Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableEq DecidableEq Monoid MulAction

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Finsetstatement · cited by 13,712
Monoidstatement and proof · cited by 3,887
MulActionstatement and proof · cited by 1,294
Finset.monoidstatement · cited by 20

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.