Equations
- squarefree w = ∀ l < w.length, ∀ (v : Mathlib.Vector (Fin 2) l), ↑v ≠ [] → ¬↑v ++ ↑v <:+: ↑w
Instances For
Equations
- instDecidableSquarefree w = w.length.decidableBallLT fun (n : ℕ) (x : n < w.length) => ∀ (v : Mathlib.Vector (Fin 2) n), ↑v ≠ [] → ¬↑v ++ ↑v <:+: ↑w