dpEqualizer_is_dp_ideal_right — Mathlib

English

Let hI and hI' be divided-power structures on I. Then the right equalizer dpEqualizer(hI,hI') is a sub-divided-power-ideal of hI'.

Русский

Пусть hI и hI' — структуру разделённых степеней на I. Тогда правыйdpEqualizer(hI,hI') образует подDP-идеал в hI'.

LaTeX

$$$IsSubDPIdeal(hI',\\ dpEqualizer(hI,hI'))$$$

Lean4

theorem dpEqualizer_is_dp_ideal_right : DividedPowers.IsSubDPIdeal hI' (dpEqualizer hI hI') :=
  IsSubDPIdeal.mk (fun _ hx ↦ hx.1)
    (fun _ hn x hx ↦
      ⟨hI'.dpow_mem hn hx.1, fun m ↦ by rw [← hx.2, hI.dpow_comp hn hx.1, hx.2, hx.2, hI'.dpow_comp hn hx.1]⟩)

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