instIsScalarTower

Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

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

English

Equality in FiniteAdeleRing is determined componentwise along v.

Русский

Равенство в FiniteAdeleRing определяется по компонентам вдоль v.

LaTeX

$$([ext] {a1 a2 : FiniteAdeleRing R K})$$

Lean4

instance : IsScalarTower R K (FiniteAdeleRing R K) :=
  IsScalarTower.of_algebraMap_eq' rfl

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

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

Разделы

Аффилиация

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