numerator_isUnit

Mathlib.GroupTheory.OreLocalization.Basic

URI: https://scilib.ai/kg/mathlib#OreLocalization.numerator_isUnit

English

For s ∈ S, the image numeratorHom(s) is a unit in the localization.

Русский

Образ numeratorHom(s) является единицей в локализации.

LaTeX

$$$\\text{IsUnit}(\\text{numeratorHom}(s))$$$

Lean4

@[to_additive]
theorem numerator_isUnit (s : S) : IsUnit (numeratorHom (s : R) : R[S⁻¹]) :=
  ⟨numeratorUnit s, rfl⟩

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

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

Разделы

Аффилиация

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