lift_eq — Mathlib

English

Let A be an additive commutative monoid, and F : AwayMap x B a localization map away from x. If g: A →+ C is an additive monoid homomorphism with g(x) an additive unit, then for any a ∈ A, F.lift x hg (F a) = g a.

Русский

Пусть A — аддитивный коммутативный моноид, F : AwayMap x B — локализационная карта away от x. Если g: A →+ C — аддитивный моноид-гомоморфизм с тем, что g(x) является аддитивной единицей, то для любого a ∈ A выполняется F.lift x hg (F a) = g a.

LaTeX

$$$ F.lift x\ hg (F a) = g a $$$

Lean4

@[simp]
theorem lift_eq (hg : IsAddUnit (g x)) (a : A) : F.lift x hg (F a) = g a :=
  AddSubmonoid.LocalizationMap.lift_eq _ _ _

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