card_le_card_of_submodule — Mathlib

English

If N ≤ M is a submodule and b is a basis of M, while b' is a basis of N (in the submodule sense), then the index set of b' has cardinality at most that of b: |ι'| ≤ |ι|.

Русский

Если N подмодуль M и b — базис M, a b' — базис N, то |ι'| ≤ |ι|.

LaTeX

$$|\\iota'| \\le |\\iota|$$

Lean4

theorem card_le_card_of_submodule (N : Submodule R M) [Fintype ι] (b : Basis ι R M) [Fintype ι'] (b' : Basis ι' R N) :
    Fintype.card ι' ≤ Fintype.card ι :=
  b.card_le_card_of_linearIndependent (b'.linearIndependent.map_injOn N.subtype N.injective_subtype.injOn)

Похожие утверждения