finite_iff_of_rank_eq_nsmul — Mathlib

English

Given W with rank, if rank M equals n times rank W for some nonzero n, then M is finite iff W is finite.

Русский

Пусть W имеет ранг, тогда если rank_R(M) = n • rank_R(W) для некоторого n ≠ 0, то M конечен по R тогда и только тогда, когда W конечен по R.

LaTeX

$$$$ (\\exists n\\in\\mathbb{N}, n \\neq 0) \\; \\&\\& \\; Module.rank\\,R\\,M = n\\cdot Module.rank\\,R\\,W \\;\\rightarrow\\; (Module.Finite\\,R\\,M \\leftrightarrow Module.Finite\\,R\\,W) $$$$

Lean4

theorem finite_iff_of_rank_eq_nsmul {W} [AddCommMonoid W] [Module R W] [Module.Free R W] {n : ℕ} (hn : n ≠ 0)
    (hVW : Module.rank R M = n • Module.rank R W) : Module.Finite R M ↔ Module.Finite R W := by
  simp only [← rank_lt_aleph0_iff, hVW, nsmul_lt_aleph0_iff_of_ne_zero hn]

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