awayToAwayRight

Mathlib.GroupTheory.MonoidLocalization.Away

URI: https://scilib.ai/kg/mathlib#AddSubmonoid.LocalizationMap.awayToAwayRight

Lean4

/-- Given `x y : A` and Localization maps `F : A →+ B, G : A →+ C` away from `x` and `x + y`
respectively, the homomorphism induced from `B` to `C`. -/
noncomputable def awayToAwayRight (y : A) (G : AwayMap (x + y) C) : B →+ C :=
  F.lift x <|
    show IsAddUnit (G x) from
      isAddUnit_of_add_eq_zero (G x) (G.mk' y ⟨x + y, mem_multiples _⟩) <| by rw [add_mk'_eq_mk'_of_add, mk'_self]

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

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

Разделы

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

Аффилиация

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