inclusion

Mathlib.RingTheory.Valuation.ValuationSubring

URI: https://scilib.ai/kg/mathlib#ValuationSubring.inclusion

English

The canonical ring homomorphism induced by inclusion when R ≤ S.

Русский

Каноническое кольцевое гомоморфизмо, индуцированное включением при условии R ≤ S.

LaTeX

$$$inclusion(R,S,h): R \to S$ is a ring homomorphism$$

Lean4

/-- The ring homomorphism induced by the partial order. -/
def inclusion (R S : ValuationSubring K) (h : R ≤ S) : R →+* S :=
  Subring.inclusion h

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

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

Разделы

Аффилиация

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