l : Type ?u.223607
m : Type u_2
n : Type u_3
o : Type ?u.223616
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 (m → R)
⊢ rank A ≤ Fintype.card m
l : Type ?u.223607
m : Type u_2
n : Type u_3
o : Type ?u.223616
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 m
haveI : Module.Finite R (m → R) := Module.Finite.pi
l : Type ?u.223607
m : Type u_2
n : Type u_3
o : Type ?u.223616
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 (m → R)
this : Module.Free R (m → R)
⊢ rank A ≤ Fintype.card m
l : Type ?u.223607
m : Type u_2
n : Type u_3
o : Type ?u.223616
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 (m → R)
⊢ rank A ≤ Fintype.card m
haveI : Module.Free R (m → R) := Module.Free.pi _ _
no goals
l : Type ?u.223607
m : Type u_2
n : Type u_3
o : Type ?u.223616
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 (m → R)
this : Module.Free R (m → R)
⊢ rank A ≤ Fintype.card m
exact (Submodule.finrank_le _).trans (finrank_pi R).le