le_of_fin_injective — Mathlib

English

Let R be a ring with StrongRankCondition. If f: (Fin n → R) →ₗ Fin m → R is injective, then n ≤ m.

Русский

Пусть R удовлетворяет StrongRankCondition. Если f: (Fin n → R) →ₗ Fin m → R инъективно, то n ≤ m.

LaTeX

$$$\text{Let } R \text{ be a semiring with } \text{StrongRankCondition};\; f:(\mathrm{Fin}\,n\to R)\to_\mathrm{lin} (\mathrm{Fin}\,m\to R)\;\Rightarrow\; f\text{ injective } \Rightarrow n \le m.$$$

Lean4

theorem le_of_fin_injective [StrongRankCondition R] {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R) : Injective f → n ≤ m :=
  StrongRankCondition.le_of_fin_injective f

Похожие утверждения