Theorems · Inductive type · linear algebra

Holor.CPRankMax

{α : Type} → [Mul α] → [AddMonoid α] → ℕ → {ds : List ℕ} → Holor α ds → Prop

CPRankMax N x means x has CP rank at most N, that is, it can be written as the sum of N holors of rank at most 1.

Defined in

Mathlib.Data.Holor

Cited by

8 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

MulAddMonoid