Theorems · Theorem · linear algebra

Module.Projective.exists_dual_eq_one

∀ {V : Type uV} [inst : AddCommMonoid V] (K : Type u_1) [inst_1 : Semifield K] [inst_2 : Module K V]
  [Module.Projective K V] {x : V}, x ≠ 0 → ∃ f, f x = 1

This is a linear map version of SeparatingDual.exists_eq_one in a projective module.

Defined in

Mathlib.LinearAlgebra.Dual.Lemmas

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoidSemifieldModuleModule.Projective