# mathlibdocumentation

linear_algebra.basis

# Bases #

This file defines bases in a module or vector space.

It is inspired by Isabelle/HOL's linear algebra, and hence indirectly by HOL Light.

## Main definitions #

All definitions are given for families of vectors, i.e. `v : ι → M` where `M` is the module or vector space and `ι : Type*` is an arbitrary indexing type.

• `basis ι R M` is the type of `ι`-indexed `R`-bases for a module `M`, represented by a linear equiv `M ≃ₗ[R] ι →₀ R`.

• the basis vectors of a basis `b : basis ι R M` are available as `b i`, where `i : ι`

• `basis.repr` is the isomorphism sending `x : M` to its coordinates `basis.repr x : ι →₀ R`. The converse, turning this isomorphism into a basis, is called `basis.of_repr`.

• If `ι` is finite, there is a variant of `repr` called `basis.equiv_fun b : M ≃ₗ[R] ι → R` (saving you from having to work with `finsupp`). The converse, turning this isomorphism into a basis, is called `basis.of_equiv_fun`.

• `basis.constr hv f` constructs a linear map `M₁ →ₗ[R] M₂` given the values `f : ι → M₂` at the basis elements `⇑b : ι → M₁`.

• `basis.reindex` uses an equiv to map a basis to a different indexing set.

• `basis.map` uses a linear equiv to map a basis to a different module.

## Main statements #

• `basis.mk`: a linear independent set of vectors spanning the whole module determines a basis

• `basis.ext` states that two linear maps are equal if they coincide on a basis. Similar results are available for linear equivs (if they coincide on the basis vectors), elements (if their coordinates coincide) and the functions `b.repr` and `⇑b`.

• `basis.of_vector_space` states that every vector space has a basis.

## Implementation notes #

We use families instead of sets because it allows us to say that two identical vectors are linearly dependent. For bases, this is useful as well because we can easily derive ordered bases by using an ordered index type `ι`.

## Tags #

basis, bases

structure basis (ι : Type u_1) (R : Type u_3) (M : Type u_5) [semiring R] [ M] :
Type (max u_1 u_3 u_5)

A `basis ι R M` for a module `M` is the type of `ι`-indexed `R`-bases of `M`.

The basis vectors are available as `coe_fn (b : basis ι R M) : ι → M`. To turn a linear independent family of vectors spanning `M` into a basis, use `basis.mk`. They are internally represented as linear equivs `M ≃ₗ[R] (ι →₀ R)`, available as `basis.repr`.

Instances for `basis`
@[protected, instance]
noncomputable def basis.inhabited {ι : Type u_1} {R : Type u_3} [semiring R] :
inhabited (basis ι R →₀ R))
Equations
@[protected, instance]
noncomputable def basis.has_coe_to_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] :
has_coe_to_fun (basis ι R M) (λ (_x : R M), ι → M)

`b i` is the `i`th basis vector.

Equations
@[simp]
theorem basis.coe_of_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (e : M ≃ₗ[R] ι →₀ R) :
{repr := e} = λ (i : ι), (e.symm) 1)
@[protected]
theorem basis.injective {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) [nontrivial R] :
theorem basis.repr_symm_single_one {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (i : ι) :
(b.repr.symm) 1) = b i
theorem basis.repr_symm_single {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (i : ι) (c : R) :
(b.repr.symm) c) = c b i
@[simp]
theorem basis.repr_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (i : ι) :
(b.repr) (b i) =
theorem basis.repr_self_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (i j : ι) [decidable (i = j)] :
((b.repr) (b i)) j = ite (i = j) 1 0
@[simp]
theorem basis.repr_symm_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (v : ι →₀ R) :
(b.repr.symm) v = M R b) v
@[simp]
theorem basis.coe_repr_symm {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) :
(b.repr.symm) = R b
@[simp]
theorem basis.repr_total {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (v : ι →₀ R) :
(b.repr) ( M R b) v) = v
@[simp]
theorem basis.total_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (x : M) :
M R b) ((b.repr) x) = x
theorem basis.repr_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) :
theorem basis.mem_span_repr_support {R : Type u_3} {M : Type u_5} [semiring R] [ M] {ι : Type u_1} (b : R M) (m : M) :
m (b '' (((b.repr) m).support))
theorem basis.repr_support_subset_of_mem_span {R : Type u_3} {M : Type u_5} [semiring R] [ M] {ι : Type u_1} (b : R M) (s : set ι) {m : M} (hm : m (b '' s)) :
(((b.repr) m).support) s
@[simp]
theorem basis.coord_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (i : ι) (ᾰ : M) :
(b.coord i) = ((b.repr) ᾰ) i
noncomputable def basis.coord {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (i : ι) :

`b.coord i` is the linear function giving the `i`'th coordinate of a vector with respect to the basis `b`.

`b.coord i` is an element of the dual space. In particular, for finite-dimensional spaces it is the `ι`th basis vector of the dual space.

Equations
theorem basis.forall_coord_eq_zero_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) {x : M} :
(∀ (i : ι), (b.coord i) x = 0) x = 0
noncomputable def basis.sum_coords {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) :

The sum of the coordinates of an element `m : M` with respect to a basis.

Equations
@[simp]
theorem basis.coe_sum_coords {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) :
(b.sum_coords) = λ (m : M), ((b.repr) m).sum (λ (i : ι), id)
theorem basis.coe_sum_coords_eq_finsum {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) :
(b.sum_coords) = λ (m : M), finsum (λ (i : ι), (b.coord i) m)
@[simp]
theorem basis.coe_sum_coords_of_fintype {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) [fintype ι] :
(b.sum_coords) = finset.univ.sum (λ (i : ι), (b.coord i))
@[simp]
theorem basis.sum_coords_self_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (i : ι) :
(b.sum_coords) (b i) = 1
theorem basis.ext {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) {R₁ : Type u_9} [semiring R₁] {σ : R →+* R₁} {M₁ : Type u_10} [add_comm_monoid M₁] [module R₁ M₁] {f₁ f₂ : M →ₛₗ[σ] M₁} (h : ∀ (i : ι), f₁ (b i) = f₂ (b i)) :
f₁ = f₂

Two linear maps are equal if they are equal on basis vectors.

theorem basis.ext' {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) {R₁ : Type u_9} [semiring R₁] {σ : R →+* R₁} {σ' : R₁ →+* R} [ σ'] [ σ] {M₁ : Type u_10} [add_comm_monoid M₁] [module R₁ M₁] {f₁ f₂ : M ≃ₛₗ[σ] M₁} (h : ∀ (i : ι), f₁ (b i) = f₂ (b i)) :
f₁ = f₂

Two linear equivs are equal if they are equal on basis vectors.

theorem basis.ext_elem {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) {x y : M} (h : ∀ (i : ι), ((b.repr) x) i = ((b.repr) y) i) :
x = y

Two elements are equal if their coordinates are equal.

theorem basis.repr_eq_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] {b : R M} {f : M →ₗ[R] ι →₀ R} :
(b.repr) = f ∀ (i : ι), f (b i) =
theorem basis.repr_eq_iff' {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] {b : R M} {f : M ≃ₗ[R] ι →₀ R} :
b.repr = f ∀ (i : ι), f (b i) =
theorem basis.apply_eq_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] {b : R M} {x : M} {i : ι} :
b i = x (b.repr) x =
theorem basis.repr_apply_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (f : M → ι → R) (hadd : ∀ (x y : M), f (x + y) = f x + f y) (hsmul : ∀ (c : R) (x : M), f (c x) = c f x) (f_eq : ∀ (i : ι), f (b i) = 1)) (x : M) (i : ι) :
((b.repr) x) i = f x i

An unbundled version of `repr_eq_iff`

theorem basis.eq_of_repr_eq_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] {b₁ b₂ : R M} (h : ∀ (x : M) (i : ι), ((b₁.repr) x) i = ((b₂.repr) x) i) :
b₁ = b₂

Two bases are equal if they assign the same coordinates.

@[ext]
theorem basis.eq_of_apply_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] {b₁ b₂ : R M} (h : ∀ (i : ι), b₁ i = b₂ i) :
b₁ = b₂

Two bases are equal if their basis vectors are the same.

@[protected]
noncomputable def basis.map {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (f : M ≃ₗ[R] M') :
R M'

Apply the linear equivalence `f` to the basis vectors.

Equations
@[simp]
theorem basis.map_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (f : M ≃ₗ[R] M') :
(b.map f).repr = f.symm.trans b.repr
@[simp]
theorem basis.map_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (f : M ≃ₗ[R] M') (i : ι) :
(b.map f) i = f (b i)
@[simp]
theorem basis.map_coeffs_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) {R' : Type u_9} [semiring R'] [module R' M] (f : R ≃+* R') (h : ∀ (c : R) (x : M), f c x = c x) :
noncomputable def basis.map_coeffs {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) {R' : Type u_9} [semiring R'] [module R' M] (f : R ≃+* R') (h : ∀ (c : R) (x : M), f c x = c x) :
R' M

If `R` and `R'` are isomorphic rings that act identically on a module `M`, then a basis for `M` as `R`-module is also a basis for `M` as `R'`-module.

See also `basis.algebra_map_coeffs` for the case where `f` is equal to `algebra_map`.

Equations
theorem basis.map_coeffs_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) {R' : Type u_9} [semiring R'] [module R' M] (f : R ≃+* R') (h : ∀ (c : R) (x : M), f c x = c x) (i : ι) :
(b.map_coeffs f h) i = b i
@[simp]
theorem basis.coe_map_coeffs {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) {R' : Type u_9} [semiring R'] [module R' M] (f : R ≃+* R') (h : ∀ (c : R) (x : M), f c x = c x) :
noncomputable def basis.reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (e : ι ι') :
basis ι' R M

`b.reindex (e : ι ≃ ι')` is a basis indexed by `ι'`

Equations
theorem basis.reindex_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (e : ι ι') (i' : ι') :
(b.reindex e) i' = b ((e.symm) i')
@[simp]
theorem basis.coe_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (e : ι ι') :
@[simp]
theorem basis.coe_reindex_repr {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (x : M) (e : ι ι') :
(((b.reindex e).repr) x) = ((b.repr) x) (e.symm)
@[simp]
theorem basis.reindex_repr {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (x : M) (e : ι ι') (i' : ι') :
(((b.reindex e).repr) x) i' = ((b.repr) x) ((e.symm) i')
@[simp]
theorem basis.reindex_refl {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) :
@[simp]
theorem basis.range_reindex' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (e : ι ι') :

`simp` normal form version of `range_reindex`

theorem basis.range_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (e : ι ι') :
noncomputable def basis.reindex_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) :

`b.reindex_range` is a basis indexed by `range b`, the basis vectors themselves.

Equations
theorem basis.finsupp.single_apply_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] {f : α → β} (hf : function.injective f) (x z : α) (y : γ) :
(finsupp.single (f x) y) (f z) = y) z
theorem basis.reindex_range_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (i : ι) (h : b i set.range (λ (i : ι), b i) := _) :
(b.reindex_range) b i, h⟩ = b i
theorem basis.reindex_range_repr_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (i : ι) :
@[simp]
theorem basis.reindex_range_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (x : (set.range b)) :
theorem basis.reindex_range_repr' {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (x : M) {bi : M} {i : ι} (h : b i = bi) :
((b.reindex_range.repr) x) bi, _⟩ = ((b.repr) x) i
@[simp]
theorem basis.reindex_range_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (x : M) (i : ι) (h : b i set.range (λ (i : ι), b i) := _) :
((b.reindex_range.repr) x) b i, h⟩ = ((b.repr) x) i
noncomputable def basis.reindex_finset_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) [fintype ι] :
M

`b.reindex_finset_range` is a basis indexed by `finset.univ.image b`, the finite set of basis vectors themselves.

Equations
theorem basis.reindex_finset_range_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) [fintype ι] (i : ι) (h : := _) :
@[simp]
theorem basis.reindex_finset_range_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) [fintype ι] (x : ) :
theorem basis.reindex_finset_range_repr_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) [fintype ι] (i : ι) :
@[simp]
theorem basis.reindex_finset_range_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) [fintype ι] (x : M) (i : ι) (h : := _) :
@[protected]
theorem basis.linear_independent {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) :
@[protected]
theorem basis.ne_zero {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) [nontrivial R] (i : ι) :
b i 0
@[protected]
theorem basis.mem_span {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (x : M) :
@[protected]
theorem basis.span_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) :
theorem basis.index_nonempty {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) [nontrivial M] :
noncomputable def basis.constr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (S : Type u_9) [semiring S] [ M'] [ M'] :
(ι → M') ≃ₗ[S] M →ₗ[R] M'

Construct a linear map given the value at the basis.

This definition is parameterized over an extra `semiring S`, such that `smul_comm_class R S M'` holds. If `R` is commutative, you can set `S := R`; if `R` is not commutative, you can recover an `add_equiv` by setting `S := ℕ`. See library note [bundled maps over different rings].

Equations
theorem basis.constr_def {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (S : Type u_9) [semiring S] [ M'] [ M'] (f : ι → M') :
(b.constr S) f = M' R id).comp R f).comp (b.repr))
theorem basis.constr_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (S : Type u_9) [semiring S] [ M'] [ M'] (f : ι → M') (x : M) :
((b.constr S) f) x = ((b.repr) x).sum (λ (b : ι) (a : R), a f b)
@[simp]
theorem basis.constr_basis {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (S : Type u_9) [semiring S] [ M'] [ M'] (f : ι → M') (i : ι) :
((b.constr S) f) (b i) = f i
theorem basis.constr_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (S : Type u_9) [semiring S] [ M'] [ M'] {g : ι → M'} {f : M →ₗ[R] M'} (h : ∀ (i : ι), g i = f (b i)) :
(b.constr S) g = f
theorem basis.constr_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (S : Type u_9) [semiring S] [ M'] [ M'] (f : M →ₗ[R] M') :
(b.constr S) (λ (i : ι), f (b i)) = f
theorem basis.constr_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (S : Type u_9) [semiring S] [ M'] [ M'] [nonempty ι] {f : ι → M'} :
@[simp]
theorem basis.constr_comp {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (S : Type u_9) [semiring S] [ M'] [ M'] (f : M' →ₗ[R] M') (v : ι → M') :
(b.constr S) (f v) = f.comp ((b.constr S) v)
@[protected]
noncomputable def basis.equiv {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (b' : basis ι' R M') (e : ι ι') :
M ≃ₗ[R] M'

If `b` is a basis for `M` and `b'` a basis for `M'`, and the index types are equivalent, `b.equiv b' e` is a linear equivalence `M ≃ₗ[R] M'`, mapping `b i` to `b' (e i)`.

Equations
@[simp]
theorem basis.equiv_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (i : ι) (b' : basis ι' R M') (e : ι ι') :
(b.equiv b' e) (b i) = b' (e i)
@[simp]
theorem basis.equiv_refl {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) :
b.equiv b (equiv.refl ι) =
@[simp]
theorem basis.equiv_symm {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (b' : basis ι' R M') (e : ι ι') :
(b.equiv b' e).symm = b'.equiv b e.symm
@[simp]
theorem basis.equiv_trans {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {M'' : Type u_7} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (b' : basis ι' R M') [add_comm_monoid M''] [ M''] {ι'' : Type u_4} (b'' : basis ι'' R M'') (e : ι ι') (e' : ι' ι'') :
(b.equiv b' e).trans (b'.equiv b'' e') = b.equiv b'' (e.trans e')
@[simp]
theorem basis.map_equiv {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (b' : basis ι' R M') (e : ι ι') :
b.map (b.equiv b' e) = b'.reindex e.symm
@[protected]
noncomputable def basis.prod {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (b' : basis ι' R M') :
basis ι') R (M × M')

`basis.prod` maps a `ι`-indexed basis for `M` and a `ι'`-indexed basis for `M'` to a `ι ⊕ ι'`-index basis for `M × M'`. For the specific case of `R × R`, see also `basis.fin_two_prod`.

Equations
@[simp]
theorem basis.prod_repr_inl {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (b' : basis ι' R M') (x : M × M') (i : ι) :
(((b.prod b').repr) x) (sum.inl i) = ((b.repr) x.fst) i
@[simp]
theorem basis.prod_repr_inr {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (b' : basis ι' R M') (x : M × M') (i : ι') :
(((b.prod b').repr) x) (sum.inr i) = ((b'.repr) x.snd) i
theorem basis.prod_apply_inl_fst {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (b' : basis ι' R M') (i : ι) :
((b.prod b') (sum.inl i)).fst = b i
theorem basis.prod_apply_inr_fst {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (b' : basis ι' R M') (i : ι') :
((b.prod b') (sum.inr i)).fst = 0
theorem basis.prod_apply_inl_snd {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (b' : basis ι' R M') (i : ι) :
((b.prod b') (sum.inl i)).snd = 0
theorem basis.prod_apply_inr_snd {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (b' : basis ι' R M') (i : ι') :
((b.prod b') (sum.inr i)).snd = b' i
@[simp]
theorem basis.prod_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] (b : R M) (b' : basis ι' R M') (i : ι ι') :
(b.prod b') i = sum.elim ( M M') b) ( M M') b') i
@[protected]
theorem basis.no_zero_smul_divisors {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) :
@[protected]
theorem basis.smul_eq_zero {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) {c : R} {x : M} :
c x = 0 c = 0 x = 0
theorem eq_bot_of_rank_eq_zero {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] (b : R M) (N : M) (rank_eq : ∀ {m : } (v : fin mN), (coe v)m = 0) :
N =
@[protected]
noncomputable def basis.singleton (ι : Type u_1) (R : Type u_2) [unique ι] [semiring R] :
R R

`basis.singleton ι R` is the basis sending the unique element of `ι` to `1 : R`.

Equations
@[simp]
theorem basis.singleton_apply (ι : Type u_1) (R : Type u_2) [unique ι] [semiring R] (i : ι) :
R) i = 1
@[simp]
theorem basis.singleton_repr (ι : Type u_1) (R : Type u_2) [unique ι] [semiring R] (x : R) (i : ι) :
( R).repr) x) i = x
theorem basis.basis_singleton_iff {R : Type u_1} {M : Type u_2} [ring R] [nontrivial R] [ M] (ι : Type u_3) [unique ι] :
nonempty (basis ι R M) ∃ (x : M) (H : x 0), ∀ (y : M), ∃ (r : R), r x = y
@[protected]
noncomputable def basis.empty {ι : Type u_1} {R : Type u_3} (M : Type u_5) [semiring R] [ M] [subsingleton M] [is_empty ι] :
R M

If `M` is a subsingleton and `ι` is empty, this is the unique `ι`-indexed basis for `M`.

Equations
@[protected, instance]
noncomputable def basis.empty_unique {ι : Type u_1} {R : Type u_3} (M : Type u_5) [semiring R] [ M] [subsingleton M] [is_empty ι] :
unique (basis ι R M)
Equations
noncomputable def basis.equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] [fintype ι] (b : R M) :
M ≃ₗ[R] ι → R

A module over `R` with a finite basis is linearly equivalent to functions from its basis to `R`.

Equations
noncomputable def module.fintype_of_fintype {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] [fintype ι] (b : R M) [fintype R] :

A module over a finite ring that admits a finite basis is finite.

Equations
theorem module.card_fintype {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] [fintype ι] (b : R M) [fintype R] [fintype M] :
@[simp]
theorem basis.equiv_fun_symm_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] [fintype ι] (b : R M) (x : ι → R) :
(b.equiv_fun.symm) x = finset.univ.sum (λ (i : ι), x i b i)

Given a basis `v` indexed by `ι`, the canonical linear equivalence between `ι → R` and `M` maps a function `x : ι → R` to the linear combination `∑_i x i • v i`.

@[simp]
theorem basis.equiv_fun_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] [fintype ι] (b : R M) (u : M) :
(b.equiv_fun) u = ((b.repr) u)
@[simp]
theorem basis.map_equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] [fintype ι] (b : R M) (f : M ≃ₗ[R] M') :
theorem basis.sum_equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] [fintype ι] (b : R M) (u : M) :
finset.univ.sum (λ (i : ι), (b.equiv_fun) u i b i) = u
theorem basis.sum_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] [fintype ι] (b : R M) (u : M) :
finset.univ.sum (λ (i : ι), ((b.repr) u) i b i) = u
@[simp]
theorem basis.equiv_fun_self {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] [fintype ι] (b : R M) (i j : ι) :
(b.equiv_fun) (b i) j = ite (i = j) 1 0
noncomputable def basis.of_equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] [fintype ι] (e : M ≃ₗ[R] ι → R) :
R M

Define a basis by mapping each vector `x : M` to its coordinates `e x : ι → R`, as long as `ι` is finite.

Equations
@[simp]
theorem basis.of_equiv_fun_repr_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] [fintype ι] (e : M ≃ₗ[R] ι → R) (x : M) (i : ι) :
(.repr) x) i = e x i
@[simp]
theorem basis.coe_of_equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] [fintype ι] (e : M ≃ₗ[R] ι → R) :
= λ (i : ι), (e.symm) i 1)
@[simp]
theorem basis.of_equiv_fun_equiv_fun {ι : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M] [fintype ι] (v : R M) :
@[simp]
theorem basis.constr_apply_fintype {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [semiring R] [ M] [add_comm_monoid M'] [ M'] [fintype ι] (b : R M) (S : Type u_9) [semiring S] [ M'] [ M'] (f : ι → M') (x : M) :
((b.constr S) f) x = finset.univ.sum (λ (i : ι), (b.equiv_fun) x i f i)
noncomputable def basis.equiv' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [ M] [add_comm_monoid M'] [ M'] (b : R M) (b' : basis ι' R M') (f : M → M') (g : M' → M) (hf : ∀ (i : ι), f (b i) ) (hg : ∀ (i : ι'), g (b' i) ) (hgf : ∀ (i : ι), g (f (b i)) = b i) (hfg : ∀ (i : ι'), f (g (b' i)) = b' i) :
M ≃ₗ[R] M'

If `b` is a basis for `M` and `b'` a basis for `M'`, and `f`, `g` form a bijection between the basis vectors, `b.equiv' b' f g hf hg hgf hfg` is a linear equivalence `M ≃ₗ[R] M'`, mapping `b i` to `f (b i)`.

Equations
@[simp]
theorem basis.equiv'_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [ M] [add_comm_monoid M'] [ M'] (b : R M) (b' : basis ι' R M') (f : M → M') (g : M' → M) (hf : ∀ (i : ι), f (b i) ) (hg : ∀ (i : ι'), g (b' i) ) (hgf : ∀ (i : ι), g (f (b i)) = b i) (hfg : ∀ (i : ι'), f (g (b' i)) = b' i) (i : ι) :
(b.equiv' b' f g hf hg hgf hfg) (b i) = f (b i)
@[simp]
theorem basis.equiv'_symm_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [ M] [add_comm_monoid M'] [ M'] (b : R M) (b' : basis ι' R M') (f : M → M') (g : M' → M) (hf : ∀ (i : ι), f (b i) ) (hg : ∀ (i : ι'), g (b' i) ) (hgf : ∀ (i : ι), g (f (b i)) = b i) (hfg : ∀ (i : ι'), f (g (b' i)) = b' i) (i : ι') :
((b.equiv' b' f g hf hg hgf hfg).symm) (b' i) = g (b' i)
theorem basis.sum_repr_mul_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ M] (b : R M) {ι' : Type u_2} [fintype ι'] (b' : basis ι' R M) (x : M) (i : ι) :
finset.univ.sum (λ (j : ι'), ((b.repr) (b' j)) i * ((b'.repr) x) j) = ((b.repr) x) i
theorem basis.maximal {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [ M] [nontrivial R] (b : R M) :

Any basis is a maximal linear independent set.

@[protected]
noncomputable def basis.mk {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [ M] (hli : v) (hsp : (set.range v)) :
R M

A linear independent family of vectors spanning the whole module is a basis.

Equations
@[simp]
theorem basis.mk_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [ M] {x : M} (hli : v) (hsp : (set.range v)) :
((basis.mk hli hsp).repr) x = (hli.repr) x, _⟩
theorem basis.mk_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [ M] (hli : v) (hsp : (set.range v)) (i : ι) :
(basis.mk hli hsp) i = v i
@[simp]
theorem basis.coe_mk {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [ M] (hli : v) (hsp : (set.range v)) :
(basis.mk hli hsp) = v
theorem basis.mk_coord_apply_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [ M] {hli : v} {hsp : (set.range v)} (i : ι) :
((basis.mk hli hsp).coord i) (v i) = 1

Given a basis, the `i`th element of the dual basis evaluates to 1 on the `i`th element of the basis.

theorem basis.mk_coord_apply_ne {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [ M] {hli : v} {hsp : (set.range v)} {i j : ι} (h : j i) :
((basis.mk hli hsp).coord i) (v j) = 0

Given a basis, the `i`th element of the dual basis evaluates to 0 on the `j`th element of the basis if `j ≠ i`.

theorem basis.mk_coord_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [ M] {hli : v} {hsp : (set.range v)} {i j : ι} :
((basis.mk hli hsp).coord i) (v j) = ite (j = i) 1 0

Given a basis, the `i`th element of the dual basis evaluates to the Kronecker delta on the `j`th element of the basis.

@[protected]
noncomputable def basis.span {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [ M] (hli : v) :
R (set.range v))

A linear independent family of vectors is a basis for their span.

Equations
@[protected]
theorem basis.span_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [ M] (hli : v) (i : ι) :
((basis.span hli) i) = v i
theorem basis.group_smul_span_eq_top {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [ M] {G : Type u_2} [group G] [ R] [ M] [ M] {v : ι → M} (hv : (set.range v) = ) {w : ι → G} :
(set.range (w v)) =
noncomputable def basis.group_smul {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [ M] {G : Type u_2} [group G] [ R] [ M] [ M] [ M] (v : R M) (w : ι → G) :
R M

Given a basis `v` and a map `w` such that for all `i`, `w i` are elements of a group, `group_smul` provides the basis corresponding to `w • v`.

Equations
theorem basis.group_smul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [ M] {G : Type u_2} [group G] [ R] [ M] [ M] [ M] {v : R M} {w : ι → G} (i : ι) :
(v.group_smul w) i = (w v) i
theorem basis.units_smul_span_eq_top {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [ M] {v : ι → M} (hv : (set.range v) = ) {w : ι → Rˣ} :
(set.range (w v)) =
noncomputable def basis.units_smul {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [ M] (v : R M) (w : ι → Rˣ) :
R M

Given a basis `v` and a map `w` such that for all `i`, `w i` is a unit, `smul_of_is_unit` provides the basis corresponding to `w • v`.

Equations
theorem basis.units_smul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [ M] {v : R M} {w : ι → Rˣ} (i : ι) :
(v.units_smul w) i = w i v i
noncomputable def basis.is_unit_smul {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [ M] (v : R M) {w : ι → R} (hw : ∀ (i : ι), is_unit (w i)) :
R M

A version of `smul_of_units` that uses `is_unit`.

Equations
theorem basis.is_unit_smul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [ M] {v : R M} {w : ι → R} (hw : ∀ (i : ι), is_unit (w i)) (i : ι) :
(v.is_unit_smul hw) i = w i v i
noncomputable def basis.mk_fin_cons {R : Type u_3} {M : Type u_5} [ring R] [ M] {n : } {N : M} (y : M) (b : basis (fin n) R N) (hli : ∀ (c : R) (x : M), x Nc y + x = 0c = 0) (hsp : ∀ (z : M), ∃ (c : R), z + c y N) :
basis (fin (n + 1)) R M

Let `b` be a basis for a submodule `N` of `M`. If `y : M` is linear independent of `N` and `y` and `N` together span the whole of `M`, then there is a basis for `M` whose basis vectors are given by `fin.cons y b`.

Equations
@[simp]
theorem basis.coe_mk_fin_cons {R : Type u_3} {M : Type u_5} [ring R] [ M] {n : } {N : M} (y : M) (b : basis (fin n) R N) (hli : ∀ (c : R) (x : M), x Nc y + x = 0c = 0) (hsp : ∀ (z : M), ∃ (c : R), z + c y N) :
hli hsp) = (coe b)
noncomputable def basis.mk_fin_cons_of_le {R : Type u_3} {M : Type u_5} [ring R] [ M] {n : } {N O : M} (y : M) (yO : y O) (b : basis (fin n) R N) (hNO : N O) (hli : ∀ (c : R) (x : M), x Nc y + x = 0c = 0) (hsp : ∀ (z : M), z O(∃ (c : R), z + c y N)) :
basis (fin (n + 1)) R O

Let `b` be a basis for a submodule `N ≤ O`. If `y ∈ O` is linear independent of `N` and `y` and `N` together span the whole of `O`, then there is a basis for `O` whose basis vectors are given by `fin.cons y b`.

Equations
@[simp]
theorem basis.coe_mk_fin_cons_of_le {R : Type u_3} {M : Type u_5} [ring R] [ M] {n : } {N O : M} (y : M) (yO : y O) (b : basis (fin n) R N) (hNO : N O) (hli : ∀ (c : R) (x : M), x Nc y + x = 0c = 0) (hsp : ∀ (z : M), z O(∃ (c : R), z + c y N)) :
b hNO hli hsp) = fin.cons y, yO⟩ ((submodule.of_le hNO) b)
@[protected]
noncomputable def basis.fin_two_prod (R : Type u_1) [semiring R] :
basis (fin 2) R (R × R)

The basis of `R × R` given by the two vectors `(1, 0)` and `(0, 1)`.

Equations
@[simp]
theorem basis.fin_two_prod_zero (R : Type u_1) [semiring R] :
0 = (1, 0)
@[simp]
theorem basis.fin_two_prod_one (R : Type u_1) [semiring R] :
1 = (0, 1)
@[simp]
theorem basis.coe_fin_two_prod_repr {R : Type u_1} [semiring R] (x : R × R) :
(.repr) x) = ![x.fst, x.snd]
def submodule.induction_on_rank_aux {ι : Type u_1} {R : Type u_3} {M : Type u_5} [ring R] [is_domain R] [ M] (b : R M) (P : MSort u_2) (ih : Π (N : M), (Π (N' : M), N' NΠ (x : M), x N(∀ (c : R) (y : M), y N'c x + y = 0c = 0)P N')P N) (n : ) (N : M) (rank_le : ∀ {m : } (v : fin mN), (coe v)m n) :
P N

If `N` is a submodule with finite rank, do induction on adjoining a linear independent element to a submodule.

Equations
• n N rank_le = nat.rec (λ (N : M) (rank_le : ∀ {m : } (v : fin mN), (coe v)m 0), _.mpr (ih (λ (N : M) (N_le : N ) (x : M) (x_mem : x ) (x_ortho : ∀ (c : R) (y : M), y Nc x + y = 0c = 0), false.rec (P N) _))) (λ (n : ) (rank_ih : Π (N : M), (∀ {m : } (v : fin mN), (coe v)m n)P N) (N : M) (rank_le : ∀ {m : } (v : fin mN), (coe v)m n.succ), ih N (λ (N' : M) (N'_le : N' N) (x : M) (x_mem : x N) (x_ortho : ∀ (c : R) (y : M), y N'c x + y = 0c = 0), rank_ih N' _)) n N rank_le
noncomputable def basis.extend {K : Type u_4} {V : Type u} [ V] {s : set V} (hs : coe) :
basis (hs.extend _) K V

If `s` is a linear independent set of vectors, we can extend it to a basis.

Equations
• = _
theorem basis.extend_apply_self {K : Type u_4} {V : Type u} [ V] {s : set V} (hs : coe) (x : (hs.extend _)) :
@[simp]
theorem basis.coe_extend {K : Type u_4} {V : Type u} [ V] {s : set V} (hs : coe) :
theorem basis.range_extend {K : Type u_4} {V : Type u} [ V] {s : set V} (hs : coe) :
= hs.extend _
noncomputable def basis.sum_extend {ι : Type u_1} {K : Type u_4} {V : Type u} [ V] {v : ι → V} (hs : v) :
basis (_.extend basis.sum_extend._proof_2 \ set.range v)) K V

If `v` is a linear independent family of vectors, extend it to a basis indexed by a sum type.

Equations
theorem basis.subset_extend {K : Type u_4} {V : Type u} [ V] {s : set V} (hs : coe) :
s hs.extend _
def basis.of_vector_space_index (K : Type u_4) (V : Type u) [ V] :
set V

A set used to index `basis.of_vector_space`.

Equations
Instances for `↥basis.of_vector_space_index`
noncomputable def basis.of_vector_space (K : Type u_4) (V : Type u) [ V] :
V

Each vector space has a basis.

Equations
theorem basis.of_vector_space_apply_self (K : Type u_4) (V : Type u) [ V] (x : ) :
x = x
@[simp]
theorem basis.coe_of_vector_space (K : Type u_4) (V : Type u) [ V] :
theorem basis.of_vector_space_index.linear_independent (K : Type u_4) (V : Type u) [ V] :
theorem basis.range_of_vector_space (K : Type u_4) (V : Type u) [ V] :
theorem basis.exists_basis (K : Type u_4) (V : Type u) [ V] :
∃ (s : set V), nonempty (basis s K V)
theorem vector_space.card_fintype (K : Type u_4) (V : Type u) [ V] [fintype K] [fintype V] :
∃ (n : ), =
theorem nonzero_span_atom {K : Type u_4} {V : Type u} [ V] (v : V) (hv : v 0) :
is_atom {v})

For a module over a division ring, the span of a nonzero element is an atom of the lattice of submodules.

theorem atom_iff_nonzero_span {K : Type u_4} {V : Type u} [ V] (W : V) :
∃ (v : V) (hv : v 0), W = {v}

The atoms of the lattice of submodules of a module over a division ring are the submodules equal to the span of a nonzero element of the module.

@[protected, instance]
def submodule.is_atomistic {K : Type u_4} {V : Type u} [ V] :

The lattice of submodules of a module over a division ring is atomistic.

theorem linear_map.exists_left_inverse_of_injective {K : Type u_4} {V : Type u} {V' : Type u_8} [field K] [add_comm_group V'] [ V] [ V'] (f : V →ₗ[K] V') (hf_inj : = ) :
∃ (g : V' →ₗ[K] V),
theorem submodule.exists_is_compl {K : Type u_4} {V : Type u} [field K] [ V] (p : V) :
∃ (q : V), q
@[protected, instance]
def module.submodule.complemented_lattice {K : Type u_4} {V : Type u} [field K] [ V] :
theorem linear_map.exists_right_inverse_of_surjective {K : Type u_4} {V : Type u} {V' : Type u_8} [field K] [add_comm_group V'] [ V] [ V'] (f : V →ₗ[K] V') (hf_surj : = ) :
∃ (g : V' →ₗ[K] V),
theorem linear_map.exists_extend {K : Type u_4} {V : Type u} {V' : Type u_8} [field K] [add_comm_group V'] [ V] [ V'] {p : V} (f : p →ₗ[K] V') :
∃ (g : V →ₗ[K] V'), g.comp p.subtype = f

Any linear map `f : p →ₗ[K] V'` defined on a subspace `p` can be extended to the whole space.

theorem submodule.exists_le_ker_of_lt_top {K : Type u_4} {V : Type u} [field K] [ V] (p : V) (hp : p < ) :
∃ (f : V →ₗ[K] K) (H : f 0),

If `p < ⊤` is a subspace of a vector space `V`, then there exists a nonzero linear map `f : V →ₗ[K] K` such that `p ≤ ker f`.

theorem quotient_prod_linear_equiv {K : Type u_4} {V : Type u} [field K] [ V] (p : V) :
nonempty (((V p) × p) ≃ₗ[K] V)