submonoid_map_le_is_unit

Mathlib.RingTheory.Localization.InvSubmonoid

URI: https://scilib.ai/kg/mathlib#IsLocalization.submonoid_map_le_is_unit

← MathLib Explorer

English

Under a localization, every image of M in S becomes a unit in S.

Русский

В локализации каждое изображение элемента M в S становится единицей в S.

LaTeX

$$$M.map(\mathrm{algebraMap}\,R\,S) \le \mathrm{IsUnit}.submonoid\,S$$$

Lean4

theorem submonoid_map_le_is_unit : M.map (algebraMap R S) ≤ IsUnit.submonoid S :=
  by
  rintro _ ⟨a, ha, rfl⟩
  exact IsLocalization.map_units S ⟨_, ha⟩

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

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

Разделы

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

Аффилиация

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