instAlgebra

Mathlib.Topology.Algebra.Valued.WithVal

URI: https://scilib.ai/kg/mathlib#WithVal.instAlgebra

English

If S is a ring with a ring homomorphism from R and algebra structure, then WithVal v becomes an Algebra over S.

Русский

Если имеется структура алгебры над S над R, то WithVal v становится алгеброй над S.

LaTeX

$$$Algebra S (WithVal v)$$$

Lean4

instance [CommSemiring S] [CommRing R] [Algebra S R] (v : Valuation R Γ₀) : Algebra S (WithVal v) :=
  inferInstanceAs (Algebra S R)

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

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

Разделы

Аффилиация

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