Theorems · Definition · number theory
List.fixedLengthDigits
{b : ℕ} → 1 < b → ℕ → Finset (List ℕ)The set of lists of natural integers of length l with coefficients < b as a Finset.
This can be seen as the set of lists of length l of the digits in base b of
the integers < b ^ l.
Having this set as a Finset can be helpful for some proofs.
- Defined in
- Mathlib.Data.Nat.Digits.Lemmas
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- Fintypeproof · cited by 7,736
- Set.Elemproof · cited by 7,166
- Set.ofPredproof · cited by 6,101
- Set.toFinsetproof · cited by 217
- Nat.ofDigitsproof · cited by 61
- Set.MapsTo.restrictproof · cited by 57
- Fintype.ofInjectiveproof · cited by 3
- Nat.mapsTo_ofDigitsproof · cited by 2
Cited by14
Results whose statement or proof uses this declaration.
- List.consFixedLengthDigitsproof · cited by 6
- List.mem_fixedLengthDigits_iffstatement · cited by 4
- Nat.bijOn_ofDigits'statement · cited by 2
- List.ne_empty_of_mem_consFixedLengthDigitsproof · cited by 1
- List.cons_mem_fixedLengthDigits_succstatement and proof · cited by 1
- List.consFixedLengthDigits_headproof · cited by 1
- List.fixedLengthDigits.congr_simpstatement and proof · cited by 1
- List.card_fixedLengthDigitsstatement · cited by 1
- List.fixedLengthDigits_onestatement · cited by 1
- List.fixedLengthDigits_succ_eq_disjiUnionstatement and proof · cited by 1
- List.fixedLengthDigits_zerostatement · cited by 1
- List.sum_fixedLengthDigits_sumstatement and proof · cited by 1