pi_iff — Mathlib

English

If there exists a linear equivalence e: M ≃ₗ[R] N and M is finite, then N is finite.

Русский

Если имеется линейное эквивалентное отображение e: M ≃ₗ[R] N и M конечен, то N конечен.

LaTeX

$$$\\forall e:\\, M \\simeq_{R} N,\\; \\text{Module.Finite } R M \\Rightarrow \\text{Module.Finite } R N$$$

Lean4

theorem pi_iff {ι : Type*} {M : ι → Type*} [_root_.Finite ι] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)] :
    Module.Finite R (∀ i, M i) ↔ ∀ i, Module.Finite R (M i) :=
  ⟨fun _ i => of_pi M i, fun _ => inferInstance⟩

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