Theorems · Definition · number theory
List.consFixedLengthDigits
{b : ℕ} → 1 < b → ℕ → ℕ → Finset (List ℕ)The Finset of lists whose head is a fixed integer d and tail is a list
in List.fixedLengthDigits b l.
- Defined in
- Mathlib.Data.Nat.Digits.Lemmas
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- Finset.imageproof · cited by 910
- List.fixedLengthDigitsproof · cited by 13
Cited by6
Results whose statement or proof uses this declaration.
- List.pairwiseDisjoint_consFixedLengthDigitsstatement and proof · cited by 2
- List.ne_empty_of_mem_consFixedLengthDigitsstatement and proof · cited by 1
- List.consFixedLengthDigits_headstatement and proof · cited by 1
- List.fixedLengthDigits_succ_eq_disjiUnionstatement and proof · cited by 1
- List.sum_fixedLengthDigits_sumproof · cited by 1
- List.consFixedLengthDigits.congr_simpstatement and proof · cited by 0