op_bot

Mathlib.Algebra.Algebra.Subalgebra.MulOpposite

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

English

The opposite of the bottom subalgebra is the bottom subalgebra: (⊥ : Subalgebra R A).op = ⊥.

Русский

Противоположная нижняя подалгебра равна нижней: (⊥ : Subalgebra R A).op = ⊥.

LaTeX

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

Lean4

@[simp]
theorem op_bot : (⊥ : Subalgebra R A).op = ⊥ :=
  opEquiv.map_bot

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

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

Разделы

Аффилиация

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