Theorems · Theorem · linear algebra
Submodule.finrank_mono
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
{s t : Submodule R M} [Module.Finite R ↥t], s ≤ t → Module.finrank R ↥s ≤ Module.finrank R ↥t- Cited by
- 11 results in Mathlib
- Foundations
- Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound
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
- Submodulestatement and proof · cited by 7,192
- Module.finrankstatement · cited by 1,770
- Module.Finitestatement and proof · cited by 1,032
- StrongRankConditionstatement and proof · cited by 286
- Module.rank_lt_aleph0proof · cited by 23
- Cardinal.toNat_le_toNatproof · cited by 14
- Submodule.rank_monoproof · cited by 11
Cited by11
Results whose statement or proof uses this declaration.
- RootPairing.isCompl_rootSpan_ker_rootFormproof · cited by 4
- LinearEquiv.finrank_fixedSubmodule_add_leproof · cited by 2
- RootPairing.finrank_range_polarization_eq_finrank_span_corootproof · cited by 2
- Module.End.pos_finrank_genEigenspace_of_hasEigenvalueproof · cited by 1
- AddSubgroup.finrank_eq_of_finiteIndexproof · cited by 1
- Matrix.rank_add_rank_le_card_of_mul_eq_zeroproof · cited by 1
- Matrix.rank_submatrix_leproof · cited by 1
- LinearMap.finrank_genEigenspace_leproof · cited by 1
- RootPairing.polarizationIn_Injectiveproof · cited by 1
- Set.finrank_monoproof · cited by 0
- AffineIndependent.card_le_card_of_subset_affineSpanproof · cited by 0