[Merged by Bors] - feat(linear_algebra/dimension): linear equiv iff eq dim #5559
Conversation
adamtopaz
added
the
awaiting-review
|
It would be nice to get, also, that equal- |
| Two finite-dimensional vector spaces are isomorphic if they have the same (finite) dimension. | ||
| -/ | ||
| theorem nonempty_linear_equiv_of_findim_eq [finite_dimensional K V] [finite_dimensional K V₂] | ||
| (cond : findim K V = findim K V₂) : nonempty (V ≃ₗ[K] V₂) := |
There was a problem hiding this comment.
Can we get dim K V = dim K V₂ from cond using findim_eq_dim, then apply nonempty_linear_equiv_of_dim_eq?
There was a problem hiding this comment.
No, there are universe issues with this, while V and V_2 can be in different universe levels.
There was a problem hiding this comment.
The point is that dim K V = dim K W only makes sense when V and W are in the same universe.
There was a problem hiding this comment.
I added lift_dim_eq versions to the dim lemmas, and used them to golf the findim lemmas.
|
bors r+ |
github-actions
bot
added
ready-to-merge
See related zulip discussion https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Classification.20of.20finite-dimensional.20vector.20spaces/near/221357275 Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded! And happy new year! 🎉 |
bors
bot
changed the title
…ed finite-dimensionality lemmas (#5580) Two groups of lemmas about finite-dimensional normed spaces: - normed spaces of the same finite dimension are continuously linearly equivalent (this is a continuation of #5559) - variations on the existing lemma `submodule.findim_add_inf_findim_orthogonal`, that the dimensions of a subspace and its orthogonal complement sum to the dimension of the full space.
See related zulip discussion https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Classification.20of.20finite-dimensional.20vector.20spaces/near/221357275 Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
…ed finite-dimensionality lemmas (#5580) Two groups of lemmas about finite-dimensional normed spaces: - normed spaces of the same finite dimension are continuously linearly equivalent (this is a continuation of #5559) - variations on the existing lemma `submodule.findim_add_inf_findim_orthogonal`, that the dimensions of a subspace and its orthogonal complement sum to the dimension of the full space.
See related zulip discussion
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Classification.20of.20finite-dimensional.20vector.20spaces/near/221357275