@[reducible]

def Fintype.piFinsetConst {α : Type u_1} (s : Finset α) (n : ℕ) : Finset (Fin n → α)

Equations

• s^^n = Fintype.piFinset fun (x : Fin n) => s

def Fintype.«term_^^_» : Lean.TrailingParserDescr

Equations

• Fintype.«term_^^_» = Lean.ParserDescr.trailingNode `Fintype.term_^^_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^^") (Lean.ParserDescr.cat `term 71))

theorem Finset.Nonempty.piFinsetConst {α : Type u_1} {s : Finset α} {n : ℕ} (hs : s.Nonempty) : (s^^n).Nonempty

@[simp]

theorem Fintype.card_piFinsetConst {α : Type u_1} (s : Finset α) (n : ℕ) : (s^^n).card = s.card ^ n