coe_restrictScalars'

Mathlib.Algebra.Algebra.Tower

URI: https://scilib.ai/kg/mathlib#AlgHom.coe_restrictScalars'

English

Restriction of scalars preserves the algebraic equivalence class on the underlying ring.

Русский

Ограничение по скалярам сохраняет эквивалентность на уровне кольцевых гомоморфизмов.

LaTeX

$$$ (restrictScalars\ R\ f) = f \quad\text{in underlying ring structures}$$$

Lean4

@[simp]
theorem coe_restrictScalars' (f : A →ₐ[S] B) : (restrictScalars R f : A → B) = f :=
  rfl

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

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

Разделы

Аффилиация

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