Theorems · Theorem · number theory

Nat.bijOn_ofDigits

∀ {b : ℕ}, 1 < b → ∀ (l : ℕ), Set.BijOn (Nat.ofDigits b) {L | L.length = l ∧ ∀ x ∈ L, x < b} {n | n < b ^ l}

The map L ↦ Nat.ofDigits b L is bijection between the set of lists of natural integers of length l with coefficients < b to the set of natural integers < b ^ l.

Defined in

Mathlib.Data.Nat.Digits.Lemmas

Cited by

2 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound