Theorems · Theorem · linear algebra

lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank

∀ (K : Type u) (V : Type v) [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [Module.Free K V] [Module.Finite K V],
  Cardinal.lift.{u, v} (Cardinal.mk V) = Cardinal.lift.{v, u} (Cardinal.mk K) ^ Cardinal.lift.{u, v} (Module.rank K V)

Defined in

Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingStrongRankConditionAddCommGroupModuleModule.FreeModule.Finite