Theorems · Theorem · linear algebra

Module.finite_dual_iff

∀ (K : Type uK) {V : Type uV} [inst : CommSemiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [Module.Free K V], Module.Finite K (Module.Dual K V) ↔ Module.Finite K V

For an example of a non-free projective K-module V for which the forward implication fails, see https://stacks.math.columbia.edu/tag/05WG#comment-9913.

Defined in

Mathlib.LinearAlgebra.Dual.Lemmas

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleModule.Free