equiv_iff

Mathlib.RingTheory.Finiteness.Basic

URI: https://scilib.ai/kg/mathlib#Module.Finite.equiv_iff

English

If M ≃ₗ[R] N, then M finite over R iff N finite over R.

Русский

Если M эквивалентно N линейно, то M конечен над R тогда и только тогда N конечен над R.

LaTeX

$$$\\forall (e: M \\simeq_R N),\\; Module.Finite R M \\iff Module.Finite R N$$$

Lean4

theorem equiv_iff (e : M ≃ₗ[R] N) : Module.Finite R M ↔ Module.Finite R N :=
  ⟨fun _ ↦ equiv e, fun _ ↦ equiv e.symm⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru