map_unop_one

Mathlib.Algebra.Algebra.Operations

URI: https://scilib.ai/kg/mathlib#Submodule.map_unop_one

← MathLib Explorer

English

map unop of one equals one.

Русский

map unop единицы дает единицу.

LaTeX

$$$ \operatorname Submodule.map (\operatorname{opLinearEquiv R}.symm.toLinearMap) (1) = 1 $$$

Lean4

@[simp]
theorem map_unop_one : map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (1 : Submodule R Aᵐᵒᵖ) = 1 := by
  rw [← comap_equiv_eq_map_symm, comap_op_one]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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