card_vector — Mathlib

English

For a finite type α and n, the cardinality of List.Vector α n equals card α raised to the n-th power.

Русский

Для конечного типа α и n кардинальность List.Vector α n равна card α в степени n.

LaTeX

$$$\\#(\\mathrm{List.Vector}\\, \\alpha\\, n) = (\\#\\alpha)^{n}$$$

Lean4

@[simp]
theorem card_vector [Fintype α] (n : ℕ) : Fintype.card (List.Vector α n) = Fintype.card α ^ n := by
  rw [Fintype.ofEquiv_card]; simp

Похожие утверждения