Theorems · Theorem · linear algebra

Module.finrank_zero_iff

∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Finite R M] [IsDomain R] [Module.IsTorsionFree R M], Module.finrank R M = 0 ↔ Subsingleton M

A finite-dimensional space has zero finrank iff it is a subsingleton. This is the finrank version of rank_zero_iff.

Defined in

Mathlib.LinearAlgebra.Dimension.Finite

Cited by

6 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleStrongRankConditionModule.FiniteIsDomainModule.IsTorsionFree