of_equiv

Mathlib.LinearAlgebra.FreeModule.Basic

URI: https://scilib.ai/kg/mathlib#Module.Free.of_equiv

English

If e: M ≃ₗ[R] N and M is free, then N is free.

Русский

Если есть линейное эквивалентное отображение e между M и N и M свободен, то N свободен.

LaTeX

$$$$ (e:\ M \simeq_\ R\ N) \;\Big( \text{Module.Free } R M \Big) \Rightarrow \mathrm{Module.Free } R N $$$$

Lean4

theorem of_equiv (e : M ≃ₗ[R] N) : Module.Free R N :=
  of_basis <| (chooseBasis R M).map e

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

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

Разделы

Аффилиация

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