English
The CP rank of a holor x is the smallest n such that x can be written as a sum of n holors of rank at most 1.
Русский
CP-ранг холора x есть наименьшее n такое, что x можно представить как сумму из n холоров ранга не более 1.
LaTeX
$$$$ \\text{cprank}(x) = \\min\\{ n : \\text{CPRankMax } n x \\} $$$$
Lean4
/-- The CP rank of a holor `x`: the smallest N such that
`x` can be written as the sum of N holors of rank at most 1. -/
noncomputable def cprank [Ring α] (x : Holor α ds) : Nat :=
@Nat.find (fun n => CPRankMax n x) (Classical.decPred _) ⟨ds.prod, cprankMax_upper_bound x⟩
