English
For finsupp versions in a RankCondition ring, if a linear map f : Finsupp α R → Finsupp β R is injective, then card α ≤ card β.
Русский
Для версии Finsupp в кольце с RankCondition, если линейное отображение f: Finsupp α R → Finsupp β R инъективно, то |α| ≤ |β|.
LaTeX
$$$\text{If } f:(\mathrm{Finsupp}(\alpha, R)) \to_\mathrm{lin} (\mathrm{Finsupp}(\beta, R)) \text{ is injective, then } |\alpha| \le |\beta|. $$$
Lean4
theorem card_le_of_injective' [StrongRankCondition R] {α β : Type*} [Fintype α] [Fintype β] (f : (α →₀ R) →ₗ[R] β →₀ R)
(i : Injective f) : Fintype.card α ≤ Fintype.card β :=
by
let P := Finsupp.linearEquivFunOnFinite R R β
let Q := (Finsupp.linearEquivFunOnFinite R R α).symm
exact card_le_of_injective R ((P.toLinearMap.comp f).comp Q.toLinearMap) ((P.injective.comp i).comp Q.injective)
