English
There is a natural equivalence between the set of functions from Fin n to Fin m and Fin (m^n). This is a canonical finite-structure bijection.
Русский
Существует естественная биекция между множеством функций из Fin n в Fin m и Fin (m^n).
LaTeX
$$$$ (\\mathrm{Fin} n \\to \\mathrm{Fin} m) \\simeq \\mathrm{Fin}(m^n). $$$$
Lean4
/-- Equivalence between `Fin n → Fin m` and `Fin (m ^ n)`. -/
@[simps!]
def finFunctionFinEquiv {m n : ℕ} : (Fin n → Fin m) ≃ Fin (m ^ n) :=
Equiv.ofRightInverseOfCardLE (le_of_eq <| by simp_rw [Fintype.card_fun, Fintype.card_fin])
(fun f =>
⟨∑ i, f i * m ^ (i : ℕ), by
induction n with
| zero => simp
| succ n ih =>
cases m
· exact isEmptyElim (f <| Fin.last _)
simp_rw [Fin.sum_univ_castSucc, Fin.coe_castSucc, Fin.val_last]
refine (Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _ (Fin.is_le _)).trans_eq ?_
rw [← one_add_mul (_ : ℕ), add_comm, pow_succ']⟩)
(fun a b =>
⟨a / m ^ (b : ℕ) % m, by
rcases n with - | n
· exact b.elim0
rcases m with - | m
· rw [zero_pow n.succ_ne_zero] at a
exact a.elim0
· exact Nat.mod_lt _ m.succ_pos⟩)
fun a => by
dsimp
induction n with
| zero => subsingleton [(finCongr <| pow_zero _).subsingleton]
| succ n ih =>
simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
ext
simp_rw [Fin.sum_univ_succ, Fin.val_zero, Fin.val_succ, pow_zero, Nat.div_one, mul_one, pow_succ', ←
Nat.div_div_eq_div_mul, mul_left_comm _ m, ← mul_sum]
rw [ih _ (Nat.div_lt_of_lt_mul (a.is_lt.trans_eq (pow_succ' _ _))), Nat.mod_add_div]
