instAlgebra_1 — Mathlib

English

There is a natural algebra structure of 𝓞_K over any L that is a K-algebra.

Русский

Существует естественная структура алгебры 𝓞_K над любым кольцом L, являющимся алгеброй над K.

LaTeX

$$$\text{If } L \text{ is a ring and a } K\text{-algebra, then } \mathcal{O}_K \text{ has an } L\text{-algebra structure.}$$$

Lean4

instance {L : Type*} [Ring L] [Algebra K L] : Algebra (𝓞 K) L :=
  inferInstanceAs (Algebra (integralClosure _ _) L)

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