English
Two divided-powers structures on the same ideal are equal if they agree on all elements of the ideal.
Русский
Две структуры делённых степеней на одном и том же идеале равны, если они согласованы на всех элементах идеала.
LaTeX
$$$$ \\text{DividedPowers.ext} : \\forall I,\\; (\\forall x \\in I, dpow_I(x)=dpow_I'(x)) \\Rightarrow dpow_I = dpow_I' $$$$
Lean4
/-- The canonical `DividedPowers` structure on the zero ideal -/
noncomputable def dividedPowersBot : DividedPowers (⊥ : Ideal A)
where
dpow n a := open Classical in ite (a = 0 ∧ n = 0) 1 0
dpow_null {n a}
ha := by
simp only [mem_bot] at ha
rw [if_neg]
exact not_and_of_not_left (n = 0) ha
dpow_zero
ha := by
rw [mem_bot.mp ha]
simp only [and_self, ite_true]
dpow_one ha := by simp [mem_bot.mp ha]
dpow_mem {n a} hn
_ := by
simp only [mem_bot, ite_eq_right_iff, and_imp]
exact fun _ a ↦ False.elim (hn a)
dpow_add ha
hb := by
rw [mem_bot.mp ha, mem_bot.mp hb, add_zero]
simp only [true_and, mul_ite, mul_one, mul_zero]
split_ifs with h
· simp [h]
· symm
apply sum_eq_zero
grind [mem_antidiagonal]
dpow_mul {n} _ _
hx := by
rw [mem_bot.mp hx]
simp only [mul_zero, true_and, mul_ite, mul_one]
by_cases hn : n = 0
· rw [if_pos hn, hn, if_pos rfl, _root_.pow_zero]
· simp only [if_neg hn]
mul_dpow {m n x}
hx := by
rw [mem_bot.mp hx]
simp only [true_and, mul_ite, mul_one, mul_zero, add_eq_zero]
by_cases hn : n = 0
· simp only [hn, ite_true, and_true, add_zero, choose_self, cast_one]
· rw [if_neg hn, if_neg]
exact not_and_of_not_right (m = 0) hn
dpow_comp m {n a} hn
ha := by
rw [mem_bot.mp ha]
simp only [true_and, ite_eq_right_iff, _root_.mul_eq_zero, mul_ite, mul_one, mul_zero]
by_cases hm : m = 0
· simp [hm, uniformBell_zero_left, hn]
· simp only [hm, and_false, ite_false, false_or, if_neg hn]
