instAlgebra_1

Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

URI: https://scilib.ai/kg/mathlib#IsDedekindDomain.FiniteAdeleRing.instAlgebra_1

English

The tower property holds for R, K, FiniteAdeleRing: composition of scalar actions is compatible.

Русский

Свойство башни сохраняется для R, K и конечного адела: композиция действий скаляров согласуется.

LaTeX

$$instance (R) (K) : IsScalarTower R K (IsDedekindDomain.FiniteAdeleRing R K)$$

Lean4

instance : Algebra R (FiniteAdeleRing R K) :=
  Algebra.compHom _ (algebraMap R K)

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

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

Разделы

Аффилиация

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