English
Let R be a ring with RankCondition. If α,β are finite and f : (α → R) →ₗ β → R is surjective, then card β ≤ card α.
Русский
Пусть R удовлетворяет RankCondition. Если α, β конечны, и f: (α → R) →ₗ β → R сюръективно, то card β ≤ card α.
LaTeX
$$$\text{If } f:(\alpha \to R) \to_\mathrm{lin} (\beta \to R) \text{ is surjective, then } |\beta| \le |\alpha|.$$$
Lean4
theorem card_le_of_surjective [RankCondition R] {α β : Type*} [Fintype α] [Fintype β] (f : (α → R) →ₗ[R] β → R)
(i : Surjective f) : Fintype.card β ≤ Fintype.card α :=
by
let P := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
let Q := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)
exact
le_of_fin_surjective R ((Q.symm.toLinearMap.comp f).comp P.toLinearMap)
(((LinearEquiv.symm Q).surjective.comp i).comp (LinearEquiv.surjective P))
