cardinalMk_eq_cardinalMk_field_pow_rank

English

Under the same hypotheses, the cardinality of V equals |K|^{rank_K V}. This restates the previous principle in a slightly different notation.

Русский

При тех же предположениях кардинал множества V равен |K|^{rank_K V}. Это переформулировка предыдущего принципа в ином обозначении.

LaTeX

$$$|V| = |K|^{\operatorname{rank} K V}$$$

Lean4

theorem cardinalMk_eq_cardinalMk_field_pow_rank (K V : Type u) [Ring K] [StrongRankCondition K] [AddCommGroup V]
    [Module K V] [Module.Free K V] [Module.Finite K V] : #V = #K ^ Module.rank K V := by
  simpa using lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank K V

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