Codimension

Stream: Is there code for X?

[Yaël Dillies]

We have the dimension of a vector space as docs3#set.finrank. Do we not have the codimension somewhere?

[Adam Topaz]

you can always take the dimension of a quotient.

[Yaël Dillies]

Sure. In my case, everything is finite dimensional anyway, so my question is mostly "Can I make my statement look nice by writing codim V ≤ codim W + D rather than dim W ≤ dim V + D?".