← all areas

Namespace LinearIndependent 4 theorems

• Linearly independent vectors in k^ι have a nonzero minor LinearIndependent.exists_det_submatrix_ne_zero 0 below · cited by 3 · depth 17
• Linear disjointness ascends a finite extension under a degree bound LinearIndependent.map_of_finrank_le_relfinrank_closure 0 below · cited by 2 · depth 22
• Base change to a characteristic-zero field preserves independence of endomorphisms LinearIndependent.linearMap_baseChange_of_int 0 below · cited by 1 · depth 23
• ℤ-generators of a full lattice are ℝ-independent LinearIndependent.of_forall_mem_span_exists_sum_zsmul_eq 0 below · cited by 1 · depth 32