no goals
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Fintype σ
⊢ Module.rank K (↑{s | ∀ (n : σ), ↑s n ≤ Fintype.card K - 1} →₀ K) = (#↑{s | ∀ (n : σ), ↑s n ≤ Fintype.card K - 1})
rw [rank_finsupp_self']
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Fintype σ
f : σ →₀ ℕ
⊢ f ∈ {s | ∀ (n : σ), ↑s n ≤ Fintype.card K - 1} ↔ ↑Finsupp.equivFunOnFinite f ∈ {s | ∀ (n : σ), s n < Fintype.card K}
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Fintype σ
⊢ (#↑{s | ∀ (n : σ), ↑s n ≤ Fintype.card K - 1}) = (#↑{s | ∀ (n : σ), s n < Fintype.card K})
refine' Quotient.sound ⟨Equiv.subtypeEquiv Finsupp.equivFunOnFinite fun f => _⟩
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Fintype σ
f : σ →₀ ℕ
n : σ
⊢ 1 ≤ Fintype.card K
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Fintype σ
f : σ →₀ ℕ
⊢ f ∈ {s | ∀ (n : σ), ↑s n ≤ Fintype.card K - 1} ↔ ↑Finsupp.equivFunOnFinite f ∈ {s | ∀ (n : σ), s n < Fintype.card K}
refine' forall_congr' fun n => le_tsub_iff_right _
no goals
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Fintype σ
f : σ →₀ ℕ
n : σ
⊢ 1 ≤ Fintype.card K
exact Fintype.card_pos_iff.2 ⟨0⟩