coe_toAlgHom'

Mathlib.Algebra.Algebra.Tower

URI: https://scilib.ai/kg/mathlib#IsScalarTower.coe_toAlgHom'

English

The coe of the canonical tower map from S to A is exactly the algebra map algebraMap S A.

Русский

Коэ канонического отображения башни из S в A совпадает с алгебраической картой algebraMap S A.

LaTeX

$$$ (toAlgHom\ R\ S\ A : S \to A) = algebraMap\ S\ A$$

Lean4

@[simp]
theorem coe_toAlgHom' : (toAlgHom R S A : S → A) = algebraMap S A :=
  rfl

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

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

Разделы

Аффилиация

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