Definition 2

Tag 05S3, permanent. Cite it as [Bourbaki, Tag 05S3].

Given a vector space E, the codimension (with respect to E) of a subspace F of E, denoted by $\operatorname{codim}_E F$ , or simply $\operatorname{codim} F$ , is the dimension of $E/F$ (equal to that of any supplement of F in E).

Relation (3) may then be written

(9)

\dim F + \operatorname{codim} F = \dim E.

Bourbaki puts the proof directly after the statement, so what is above is the statement and its proof together.

Cited by

Nothing.

Cites

Nothing.