ofEq_rfl

Mathlib.Algebra.Module.Submodule.Equiv

URI: https://scilib.ai/kg/mathlib#LinearEquiv.ofEq_rfl

English

The top submodule of M is linearly equivalent to M itself.

Русский

Верхний подмодуль M линейно эквивалентен самому M.

LaTeX

$$def ofTop (h : p = ⊤) : p ≃_l[R] M$$

Lean4

@[simp]
theorem ofEq_rfl : ofEq p p rfl = LinearEquiv.refl R p := by ext; rfl

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

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

Разделы

Аффилиация

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