universalHom_apply

Mathlib.RingTheory.OreLocalization.Ring

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

English

The application of universalHom to the fraction r/s equals (fS s)^{-1} times f r.

Русский

Применение universalHom к дроби r/s равно (fS s)^{-1} умножить на f r.

LaTeX

$$universalHom f fS hf (r /ₒ s) = ((fS s)^{-1} : Units T) * f r$$

Lean4

theorem universalHom_apply {r : R} {s : S} : universalHom f fS hf (r /ₒ s) = ((fS s)⁻¹ : Units T) * f r :=
  rfl

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

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

Разделы

Аффилиация

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