rank_fun' — Mathlib

English

Let η be a finite set. The dimension of the space of all functions η → R over R equals the cardinality of η.

Русский

Пусть η — конечное множество. Размерность пространства функций η → R над R равна мощности η.

LaTeX

$$$ \\operatorname{Module.rank} R (\\eta \\to R) = Fintype.card \\eta. $$$

Lean4

theorem rank_fun' : Module.rank R (η → R) = Fintype.card η := by
  rw [rank_fun_eq_lift_mul, rank_self, Cardinal.lift_one, mul_one]

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