rank_finsupp — Mathlib

English

For any ι, Module.rank_R(ι →₀ M) = #ι · Module.rank_R M (cardinal multiplication).

Русский

Для любого ι: Module.rank_R(ι →₀ M) = #ι · Module.rank_R M

LaTeX

$$$\operatorname{rank}_R(\iota \to_0 M) = \#\iota \cdot \operatorname{rank}_R M$$$

Lean4

@[simp]
theorem rank_finsupp (ι : Type w) :
    Module.rank R (ι →₀ M) = Cardinal.lift.{v} #ι * Cardinal.lift.{w} (Module.rank R M) :=
  by
  obtain ⟨⟨_, bs⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
  rw [← bs.mk_eq_rank'', ← (Finsupp.basis fun _ : ι => bs).mk_eq_rank'', Cardinal.mk_sigma, Cardinal.sum_const]

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