Theorems · Theorem · linear algebra

rank_fun_eq_lift_mul

∀ {R : Type u} {M : Type v} {η : Type u₁'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [StrongRankCondition R] [Module.Free R M] [inst_5 : Fintype η],
  Module.rank R (η → M) = ↑(Fintype.card η) * Cardinal.lift.{u₁', v} (Module.rank R M)

Defined in

Mathlib.LinearAlgebra.Dimension.Constructions

Cited by

2 results in Mathlib

Foundations

Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModuleStrongRankConditionModule.FreeFintype