no goals
R : Type u
M : Type v
N : Type w
inst✝⁹ : CommRing R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Free R N
inst✝ : Module.Finite R N
⊢ finrank R (M →ₗ[R] N) = finrank R M * finrank R N
classical
  letI := nontrivial_of_invariantBasisNumber R
  have h := LinearMap.toMatrix (chooseBasis R M) (chooseBasis R N)
  simp_rw [h.finrank_eq, FiniteDimensional.finrank_matrix,
    FiniteDimensional.finrank_eq_card_chooseBasisIndex, mul_comm]
R : Type u
M : Type v
N : Type w
inst✝⁹ : CommRing R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Free R N
inst✝ : Module.Finite R N
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
⊢ finrank R (M →ₗ[R] N) = finrank R M * finrank R N
R : Type u
M : Type v
N : Type w
inst✝⁹ : CommRing R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Free R N
inst✝ : Module.Finite R N
⊢ finrank R (M →ₗ[R] N) = finrank R M * finrank R N
letI := nontrivial_of_invariantBasisNumber R
R : Type u
M : Type v
N : Type w
inst✝⁹ : CommRing R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Free R N
inst✝ : Module.Finite R N
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
h : (M →ₗ[R] N) ≃ₗ[R] Matrix (Module.Free.ChooseBasisIndex R N) (Module.Free.ChooseBasisIndex R M) R
⊢ finrank R (M →ₗ[R] N) = finrank R M * finrank R N
R : Type u
M : Type v
N : Type w
inst✝⁹ : CommRing R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Free R N
inst✝ : Module.Finite R N
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
⊢ finrank R (M →ₗ[R] N) = finrank R M * finrank R N
have h := LinearMap.toMatrix (chooseBasis R M) (chooseBasis R N)
no goals
R : Type u
M : Type v
N : Type w
inst✝⁹ : CommRing R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Free R N
inst✝ : Module.Finite R N
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
h : (M →ₗ[R] N) ≃ₗ[R] Matrix (Module.Free.ChooseBasisIndex R N) (Module.Free.ChooseBasisIndex R M) R
⊢ finrank R (M →ₗ[R] N) = finrank R M * finrank R N
simp_rw [h.finrank_eq, FiniteDimensional.finrank_matrix,
  FiniteDimensional.finrank_eq_card_chooseBasisIndex, mul_comm]