[Merged by Bors] - feat(linear_algebra/finite_dimensional): add finrank_map_le

[fpvandoorn]

---

• depends on: [Merged by Bors] - feat(linear_algebra/dimension): generalize dim_map_le to heterogeneous universes #8800

[hrmacbeth]

The finrank equality case is pretty easy if you want it -- not sure how to generalize to the version with dims and cardinals:

lemma finrank_map_linear_equiv_eq (f : V ≃ₗ[K] V) (p : submodule K V) [finite_dimensional K p] :
  finrank K (p.map (f : V →ₗ[K] V)) = finrank K p :=
begin
  refine le_antisymm _ _,
  { exact finrank_map_le K (f : V →ₗ[K] V) p },
  { have : p = (p.map (f : V →ₗ[K] V)).map f.symm,
    { simp [← p.map_comp (f : V →ₗ[K] V) (f.symm : V →ₗ[K] V)] },
    convert finrank_map_le K (f.symm : V →ₗ[K] V) (p.map f) }
end

[fpvandoorn]

Ok, I'll add that to this PR (with the codomain replaced by V₂)

[fpvandoorn]

Your lemma is also proven by (f.of_submodule p).finrank_eq.symm. Do you think it's still worth having?

[hrmacbeth]

Oh, nice! I think it's worth having, since the short proof you found is non-obvious, but obviously use the short proof.

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - feat(linear_algebra/dimension): generalize dim_map_le to heterogeneous universes #8800

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[ChrisHughes24]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests