Theorems · Theorem · linear algebra
Submodule.exists_linearEquiv_restrict_eq
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
{W W' : Submodule K V} [FiniteDimensional K ↥W] (f : ↥W ≃ₗ[K] ↥W'), ∃ g, ∀ (x : ↥W), ↑(f x) = g ↑x- Cited by
- 0 results in Mathlib
- Foundations
- Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites28
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement and proof · cited by 18,349
- AddCommGroupstatement and proof · cited by 12,871
- Submodulestatement and proof · cited by 7,192
- LinearEquivstatement and proof · cited by 3,317
- add_zeroproof · cited by 2,707
- Cardinalproof · cited by 2,598
- FiniteDimensionalstatement and proof · cited by 1,854
- map_zeroproof · cited by 1,614
- add_commproof · cited by 1,535
- LinearEquiv.symmproof · cited by 1,461
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.