finiteDimensional_iff_of_rank_eq_nsmul

English

If V and W are K-vector spaces and rank_K V = n · rank_K W for some natural n, with n ≠ 0, then V is finite-dimensional iff W is finite-dimensional.

Русский

Если ранк_K V = n · ранк_K W при некотором n ≠ 0, тогда V конечномерно тогда же как W.

LaTeX

$$\forall {K} {V} {W} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] {n : \FinNat} (hn : n ≠ 0) (hVW : Module.rank K V = n · Module.rank K W) : FiniteDimensional K V ↔ FiniteDimensional K W$$

Lean4

theorem finiteDimensional_iff_of_rank_eq_nsmul {W} [AddCommGroup W] [Module K W] {n : ℕ} (hn : n ≠ 0)
    (hVW : Module.rank K V = n • Module.rank K W) : FiniteDimensional K V ↔ FiniteDimensional K W :=
  Module.finite_iff_of_rank_eq_nsmul hn hVW

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