toIntSubmodule_symm

Mathlib.Algebra.Module.Submodule.Lattice

URI: https://scilib.ai/kg/mathlib#AddSubgroup.toIntSubmodule_symm

English

The inverse of the AddSubgroup toIntSubmodule correspondence is the Submodule toAddSubgroup correspondence.

Русский

Обратная к toIntSubmodule связь возвращается через Submodule toAddSubgroup.

LaTeX

$$$\\text{toIntSubmodule}^{-1} = \\text{toAddSubgroup}$ (up to the isomorphism)$$

Lean4

@[simp]
theorem toIntSubmodule_symm : ⇑(AddSubgroup.toIntSubmodule.symm : _ ≃o AddSubgroup M) = Submodule.toAddSubgroup :=
  rfl

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

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

Разделы

Аффилиация

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