liftOn

Mathlib.GroupTheory.DivisibleHull

URI: https://scilib.ai/kg/mathlib#DivisibleHull.liftOn

Lean4

/-- If `f : M → ℕ+ → α` respects the equivalence on localization,
lift it to a function `DivisibleHull M → α`. -/
def liftOn {α : Type*} (x : DivisibleHull M) (f : M → ℕ+ → α)
    (h : ∀ (m m' : M) (s s' : ℕ+), mk m s = mk m' s' → f m s = f m' s') : α :=
  LocalizedModule.liftOn x (fun p ↦ f p.1 (↑ⁿ.symm p.2)) fun p p' heq ↦
    h p.1 p'.1 (↑ⁿ.symm p.2) (↑ⁿ.symm p'.2) <| by
      obtain ⟨u, hu⟩ := heq
      exact mk_eq_mk.mpr ⟨↑ⁿ.symm u, hu⟩

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

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

Разделы

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

Аффилиация

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