Theorems · Theorem · linear algebra
Submodule.eq_of_le_of_finrank_eq
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
{S₁ S₂ : Submodule K V} [FiniteDimensional K ↥S₂], S₁ ≤ S₂ → Module.finrank K ↥S₁ = Module.finrank K ↥S₂ → S₁ = S₂If a submodule is contained in a finite-dimensional submodule with the same dimension, they are equal.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 119 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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
- AddCommGroupstatement and proof · cited by 12,871
- Submodulestatement and proof · cited by 7,192
- FiniteDimensionalstatement and proof · cited by 1,854
- Module.finrankstatement and proof · cited by 1,770
- DivisionRingstatement and proof · cited by 1,062
- Eq.geproof · cited by 375
- Submodule.eq_of_le_of_finrank_leproof · cited by 10
Cited by13
Results whose statement or proof uses this declaration.
- Affine.Simplex.affineSpan_pair_eq_altitude_iffproof · cited by 2
- Subspace.dualCoannihilator_dualAnnihilator_eqproof · cited by 2
- EuclideanGeometry.eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_twoproof · cited by 2
- RootPairing.ker_rootForm_eq_dualAnnihilatorproof · cited by 1
- Affine.Triangle.altitude_replace_orthocenter_eq_affineSpanproof · cited by 1
- Subspace.dualAnnihilator_dualAnnihilator_eq_mapproof · cited by 1
- EuclideanGeometry.affineSpan_of_orthocentricSystemproof · cited by 1
- SchauderBasis.RankOneDecomposition.exists_coeffproof · cited by 1
- EuclideanGeometry.Sphere.IsTangentAt.eq_orthRadius_of_finrank_add_one_eqproof · cited by 1
- Projectivization.line_unique'proof · cited by 1
- AffineIndependent.vectorSpan_eq_of_le_of_card_eq_finrank_add_oneproof · cited by 0