coe_restrictScalars

Mathlib.Algebra.Algebra.Subalgebra.Tower

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

English

The underlying set of a restricted subalgebra equals the underlying set of the original subalgebra.

Русский

Базовое множество ограниченной подалгебры совпадает с базовым множеством исходной подалгебры.

LaTeX

$$$\bigl(\restrictScalars R U\bigr) = U$ as sets$$

Lean4

@[simp]
theorem coe_restrictScalars {U : Subalgebra S A} : (restrictScalars R U : Set A) = (U : Set A) :=
  rfl

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

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

Разделы

Аффилиация

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