theorem Nat.digits_ofDigits' (b : ℕ) (h : 1 < b) (L : List ℕ) (w₁ : ∀ l ∈ L, l < b) : b.digits (ofDigits b L) = List.rdropWhile (fun (x : ℕ) => decide (x = 0)) L

theorem Nat.nStepInduction {P : ℕ → Prop} (b : ℕ) (hb : b ≠ 0) (base : ∀ i < b, P i) (more : ∀ (y : ℕ), (∀ j < b * y, P j) → ∀ x < b, P (x + b * y)) (a : ℕ) : P a

theorem Nat.ofDigits_eq_zero_iff (b : ℕ) (L : List ℕ) (hb : b ≠ 0) : ofDigits b L = 0 ↔ ∀ l ∈ L, l = 0

theorem List.length_rdropWhile_le {α : Type u_1} (p : α → Bool) (L : List α) : (rdropWhile p L).length ≤ L.length

@[simp]

theorem List.getElem_rdropWhile {α : Type u_1} (p : α → Bool) (L : List α) (i : ℕ) {hi : i < (rdropWhile p L).length} : (rdropWhile p L)[i] = L[i]

theorem List.getElem_of_rdropWhile_le {α : Type u_1} (p : α → Bool) (L : List α) (i : ℕ) (hi : (rdropWhile p L).length ≤ i) (hi' : i < L.length) : p L[i] = true

def Vector.finBij.invFun (n m : ℕ) (i : Fin (n ^ m)) : Vector (Fin n) m

Equations

• One or more equations did not get rendered due to their size.

def Vector.finBij.toFun (n m : ℕ) (v : Vector (Fin n) m) : Fin (n ^ m)

Equations

• Vector.finBij.toFun n m v = ⟨Nat.ofDigits n (List.map (fun (x : Fin n) => ↑x) v.toList), ⋯⟩

theorem Vector.finBij.isLeftInv (n m : ℕ) (i : Fin (n ^ m)) : toFun n m (invFun n m i) = i

theorem Vector.finBij.isRightInv (n m : ℕ) (v : Vector (Fin n) m) : invFun n m (toFun n m v) = v

@[specialize #[]]

def Vector.finBij (n m : ℕ) : Fin (n ^ m) ≃ Vector (Fin n) m

Equations

• Vector.finBij n m = { toFun := Vector.finBij.invFun n m, invFun := Vector.finBij.toFun n m, left_inv := ⋯, right_inv := ⋯ }

@[implicit_reducible, specialize #[]]

instance Listed.instVector {α : Type u_1} [Listed α] (n : ℕ) : Listed (Vector α n)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

def Listed.pi (α : Type u_3) (β : Type u_4) [Listed α] [Listed β] [Inhabited β] : Listed (α → β)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Listed.instReprForall {α : Type u_1} {β : Type u_2} [Listed α] [Repr α] [Repr β] : Repr (α → β)

Equations

• Listed.instReprForall = { reprPrec := fun (f : α → β) (n : ℕ) => reprPrec (List.map (fun (a : α) => (a, f a)) (Listed.listOf α)) n }