Theorems · Theorem · linear algebra
Submodule.exists_isCompl
∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
(p : Submodule K V), ∃ q, IsCompl p q- Defined in
- Mathlib.LinearAlgebra.Basis.VectorSpace
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- DivisionRingstatement and proof · cited by 1,062
- LinearMap.kerproof · cited by 848
- Submodule.subtypeproof · cited by 480
- IsComplstatement · cited by 351
- Submodule.ker_subtypeproof · cited by 25
- LinearMap.isCompl_of_projproof · cited by 5
- LinearMap.leftInverseproof · cited by 4
- LinearMap.leftInverse_apply_of_injproof · cited by 4
Cited by7
Results whose statement or proof uses this declaration.
- Submodule.ClosedComplemented.of_finiteDimensional_quotientproof · cited by 3
- LinearMap.exists_map_addHaar_eq_smul_addHaar'proof · cited by 1
- isPathConnected_compl_of_one_lt_codimproof · cited by 1
- quotient_prod_linearEquivproof · cited by 1
- LinearMap.isClosed_range_of_isClosed_map_of_finiteDimensional_quotientproof · cited by 0
- Submodule.exists_linearEquiv_restrict_eqproof · cited by 0
- Submodule.ClosedComplemented.of_finiteDimensional_of_leproof · cited by 0