Theorems · Theorem · linear algebra

Module.surjective_piEquiv_apply_iff

∀ (ι : Type u_1) (R : Type u_2) (M : Type u_3) [inst : Finite ι] [inst_1 : CommSemiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (v : ι → M),
  Function.Surjective ⇑((Module.piEquiv ι R M) v) ↔ Submodule.span R (Set.range v) = ⊤

Defined in

Mathlib.LinearAlgebra.StdBasis

Cited by

0 results in Mathlib

Foundations

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

Assumes

FiniteCommSemiringAddCommMonoidModule