toLocalSubring_injective

Mathlib.RingTheory.Valuation.LocalSubring

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

← MathLib Explorer

English

The map from valuation subrings to local subrings is injective.

Русский

Отображение изVale Subring в LocalSubring — инъективно.

LaTeX

$$toLocalSubring_injective$$

Lean4

theorem toLocalSubring_injective : Function.Injective (ValuationSubring.toLocalSubring (K := K)) := fun _ _ h ↦
  ValuationSubring.toSubring_injective congr(($h).toSubring)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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