Theorems · Theorem · linear algebra
LinearIndependent.linearIndepOn_id
∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M], LinearIndependent R v → LinearIndepOn R id (Set.range v)- Cited by
- 14 results in Mathlib
- Foundations
- Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SemiringAddCommMonoidModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- Set.rangestatement · cited by 4,705
- LinearIndependentstatement and proof · cited by 560
- LinearIndepOnstatement · cited by 211
- LinearIndependent.compproof · cited by 41
- Set.rangeSplittingproof · cited by 23
- Set.comp_rangeSplittingproof · cited by 4
- Set.rangeSplitting_injectiveproof · cited by 2
Cited by14
Results whose statement or proof uses this declaration.
- LinearIndependent.cardinal_lift_le_rankproof · cited by 16
- Submodule.eq_top_of_finrank_eqproof · cited by 15
- LinearMap.exists_leftInverse_of_injectiveproof · cited by 6
- exists_linearIndependent_cons_of_lt_rankproof · cited by 2
- union_support_maximal_linearIndependent_eq_range_basisproof · cited by 1
- Module.Basis.mk_eq_spanRankproof · cited by 1
- MvPolynomial.exists_mem_support_not_dvd_of_forall_totalDegree_leproof · cited by 1
- le_rank_iff_exists_linearIndependentproof · cited by 1
- Algebra.FormallyUnramified.range_eq_top_of_isPurelyInseparableproof · cited by 1
- LinearIndependent.linearIndepOn_id'proof · cited by 0
- linearIndependent_iUnion_finiteproof · cited by 0
- exists_basis_of_pairing_eq_zeroproof · cited by 0