instAlgebra_2 — Mathlib

English

If S is a ring and R an algebra over S, then for any valuation w on S, WithVal w carries an algebra structure over R.

Русский

Если S — кольцо и R — алгебра над S, то для любой оценки w на S WithVal w получает структуру алгебры над R.

LaTeX

$$$Algebra R (WithVal w)$$$

Lean4

instance {S : Type*} [Ring S] [Algebra R S] (w : Valuation S Γ₀) : Algebra R (WithVal w) :=
  inferInstanceAs (Algebra R S)

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