lift'_mk — Mathlib

English

For g and h as above, lifting of mk(m,s) yields (h s).unit⁻¹ (g m).

Русский

Для g и h выше подъем через mk(m,s) даёт (h s).unit⁻¹ (g m).

LaTeX

$$$\\mathrm{lift}'(g,h)(\\mathrm{mk}(m,s)) = (h(s)).unit^{-1}.\\big(g(m)\\big).$$$

Lean4

theorem lift'_mk (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x)) (m : M) (s : S) :
    LocalizedModule.lift' S g h (LocalizedModule.mk m s) = (h s).unit⁻¹.val (g m) :=
  rfl

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