English
Two divided-powers structures on the same AddSubmonoid coincide if they agree on all elements of the ideal and satisfy the same basic laws.
Русский
Две структуры делённых степеней на одном и том же аддитивном подмодуля совпадают, если они совпадают на всех элементах идеала и удовлетворяют тем же основным законам.
LaTeX
$$$$ \\mathrm{DividedPowers.ext} \\forall I\\; (hI,hI') \\; (\\forall x\\in I, hI.dpow x = hI'.dpow x) \\Rightarrow hI = hI' $$$$
Lean4
@[ext]
theorem ext (hI : DividedPowers I) (hI' : DividedPowers I)
(h_eq : ∀ (n : ℕ) {x : A} (_ : x ∈ I), hI.dpow n x = hI'.dpow n x) : hI = hI' :=
by
obtain ⟨hI, h₀, _⟩ := hI
obtain ⟨hI', h₀', _⟩ := hI'
simp only [mk.injEq]
grind
