congr

Mathlib.RingTheory.PicardGroup

URI: https://scilib.ai/kg/mathlib#Module.Invertible.congr

English

If e: M ≃_R N is an isomorphism and M is invertible, then N is invertible as well.

Русский

Если e: M ≃ N линейное изоморфизм, и M обратим, то и N обратим.

LaTeX

$$If e: M ≃ N and M invertible, then N invertible$$

Lean4

protected theorem congr (e : M ≃ₗ[R] N) : Module.Invertible R N :=
  .right (e.symm.lTensor _ ≪≫ₗ linearEquiv R M)

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

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

Разделы

Аффилиация

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