Theorems · Definition · commutative algebra
Subspace
(R : Type u) → (M : Type v) → [inst : DivisionRing R] → [inst_1 : AddCommGroup M] → [Module R M] → Type v
Subspace of a vector space. Defined to equal Submodule.
- Defined in
- Mathlib.Algebra.Module.Submodule.Basic
- Cited by
- 56 results in Mathlib
- Foundations
- Depth 45 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- Submoduleproof · cited by 7,192
- DivisionRingstatement and proof · cited by 1,062
Cited by68
Results whose statement or proof uses this declaration.
- Subspace.dualLiftstatement and proof · cited by 9
- Subspace.quotAnnihilatorEquivstatement and proof · cited by 4
- Subspace.dualLift_of_subtypestatement and proof · cited by 3
- Subspace.finrank_add_finrank_dualAnnihilator_eqstatement and proof · cited by 3
- LinearMap.BilinForm.toLin_restrict_ker_eq_inf_kerstatement and proof · cited by 2
- Submodule.ClosedComplemented.of_isCompl_isClosedstatement and proof · cited by 2
- riesz_lemmastatement and proof · cited by 2
- Submodule.linearProjOfClosedComplstatement and proof · cited by 2
- Module.Dual.exists_extension_of_le_seminorm_realstatement and proof · cited by 2
- Submodule.prodEquivOfClosedComplstatement and proof · cited by 2
- Submodule.IsCompl.isTopCompl_of_isClosedstatement and proof · cited by 2
- LinearMap.BilinForm.finrank_add_finrank_orthogonalstatement · cited by 2