isUnit_of_dvd

Mathlib.RingTheory.Localization.Away.Basic

URI: https://scilib.ai/kg/mathlib#IsLocalization.Away.isUnit_of_dvd

English

If r divides x in R, then the image algebraMap_R^S(r) is a unit in S.

Русский

Если r делит x в R, то образ через algebraMap_R^S(r) является единицей в S.

LaTeX

$$$\\exists r:\\; r \\mid x \\Rightarrow IsUnit(\\operatorname{algebraMap}_{R,S}(r))$$$

Lean4

theorem isUnit_of_dvd {r : R} (h : r ∣ x) : IsUnit (algebraMap R S r) :=
  isUnit_of_dvd_unit (map_dvd _ h) (algebraMap_isUnit x)

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

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

Разделы

Аффилиация

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