l : Type ?u.15349
m : Type u_2
n : Type u_3
o : Type ?u.15358
R : Type u_1
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
this : Module.Finite R (n → R)
⊢ rank A ≤ Fintype.card n
l : Type ?u.15349
m : Type u_2
n : Type u_3
o : Type ?u.15358
R : Type u_1
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
⊢ rank A ≤ Fintype.card n
haveI : Module.Finite R (n → R) := Module.Finite.pi
l : Type ?u.15349
m : Type u_2
n : Type u_3
o : Type ?u.15358
R : Type u_1
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
this✝ : Module.Finite R (n → R)
this : Module.Free R (n → R)
⊢ rank A ≤ Fintype.card n
l : Type ?u.15349
m : Type u_2
n : Type u_3
o : Type ?u.15358
R : Type u_1
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
this : Module.Finite R (n → R)
⊢ rank A ≤ Fintype.card n
haveI : Module.Free R (n → R) := Module.Free.pi _ _
no goals
l : Type ?u.15349
m : Type u_2
n : Type u_3
o : Type ?u.15358
R : Type u_1
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
this✝ : Module.Finite R (n → R)
this : Module.Free R (n → R)
⊢ rank A ≤ Fintype.card n
exact A.mulVecLin.finrank_range_le.trans_eq (finrank_pi _)