rank_eq — Mathlib

English

The rank of TensorAlgebra R M equals the lift of the sum over n of (rank_R M)^n.

Русский

Ранг TensorAlgebra R M равен подъёму суммы по n от (ранг_R M)^n.

LaTeX

$$$ \operatorname{Module.rank} R (TensorAlgebra R M) = \operatorname{Cardinal.lift} (\sum_{n \in \mathbb{N}} (\operatorname{Module.rank} R M)^n) $$$

Lean4

theorem rank_eq [Nontrivial R] [Module.Free R M] :
    Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR} (sum fun n ↦ Module.rank R M ^ n) :=
  by
  let ⟨⟨κ, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
  rw [(equivFreeAlgebra b).toLinearEquiv.rank_eq, FreeAlgebra.rank_eq, mk_list_eq_sum_pow, Basis.mk_eq_rank'' b]

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