unitGroup_injective

Mathlib.RingTheory.Valuation.ValuationSubring

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

← MathLib Explorer

English

The map A ↦ A.unitGroup is injective: if A.unitGroup = B.unitGroup then A = B.

Русский

Отображение A ↦ A.unitGroup инъективно: если A.unitGroup = B.unitGroup, то A = B.

LaTeX

$$A_{\mathrm{unitGroup}} = B_{\mathrm{unitGroup}} \Rightarrow A = B$$

Lean4

theorem unitGroup_injective : Function.Injective (unitGroup : ValuationSubring K → Subgroup _) := fun A B h => by
  simpa only [le_antisymm_iff, unitGroup_le_unitGroup] using h

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

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

Разделы

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

Аффилиация

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