M : Type u
inst✝⁵ : Monoid M
G : Type u
inst✝⁴ : Group G
F : Type v
inst✝³ : Field F
inst✝² : MulSemiringAction M F
inst✝¹ : MulSemiringAction G F
m : M
inst✝ : Fintype G
⊢ Module.rank { x // x ∈ subfield G F } F ≤ ↑(Fintype.card G)
M : Type u
inst✝⁵ : Monoid M
G : Type u
inst✝⁴ : Group G
F : Type v
inst✝³ : Field F
inst✝² : MulSemiringAction M F
inst✝¹ : MulSemiringAction G F
m : M
inst✝ : Fintype G
⊢ finrank { x // x ∈ subfield G F } F ≤ Fintype.card G
rw [← Cardinal.natCast_le, finrank_eq_rank]
no goals
M : Type u
inst✝⁵ : Monoid M
G : Type u
inst✝⁴ : Group G
F : Type v
inst✝³ : Field F
inst✝² : MulSemiringAction M F
inst✝¹ : MulSemiringAction G F
m : M
inst✝ : Fintype G
⊢ Module.rank { x // x ∈ subfield G F } F ≤ ↑(Fintype.card G)
apply rank_le_card