range_algebraMap_eq

Mathlib.RingTheory.Valuation.ValuationRing

URI: https://scilib.ai/kg/mathlib#ValuationRing.range_algebraMap_eq

English

The integer subring equals the image of A under algebraMap into K.

Русский

Кольцо целых равно образу A под алгебр Maps в K.

LaTeX

$$$ (\\mathrm{valuation} A K).\\operatorname{integer} = (\\mathrm{algebraMap} A K).\\operatorname{range}$$$

Lean4

theorem range_algebraMap_eq : (valuation A K).integer = (algebraMap A K).range := by ext; exact mem_integer_iff _ _ _

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

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

Разделы

Аффилиация

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