refl_symm

Mathlib.Algebra.Module.Equiv.Defs

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

English

If e: M ≃ M₂, and f is a linear map with left/right inverses, then (mk e f h1 h2) equals e.

Русский

Если e: M ≃ M₂ и существую линейные отображения f с обратными свойствами, то конструирование mk e f h1 h2 возвращает ровно e.

LaTeX

$$$ (\text{mk } e f h_1 h_2) = e $$$

Lean4

@[simp]
theorem refl_symm [Module R M] : (refl R M).symm = LinearEquiv.refl R M :=
  rfl

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

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

Разделы

Аффилиация

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