unop_bot

Mathlib.Algebra.Algebra.Subalgebra.MulOpposite

URI: https://scilib.ai/kg/mathlib#Subalgebra.unop_bot

English

The unop of the bottom opposite is the bottom: (⊥ : Subalgebra R Aᵐᵒᵖ).unop = ⊥.

Русский

Обратное (unop) к нижней подалгебре в A^{op} есть нижняя подалгебра.

LaTeX

$$$ (\perp : \mathrm{Subalgebra}(R, A^{\mathrm{op}})).\mathrm{unop} = \perp. $$$

Lean4

@[simp]
theorem unop_bot : (⊥ : Subalgebra R Aᵐᵒᵖ).unop = ⊥ :=
  opEquiv.symm.map_bot

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

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

Разделы

Аффилиация

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