dividedPowers_unique — Mathlib

English

In a ℚ-algebra, there are no other divided power structures on an ideal; uniqueness holds.

Русский

В ℚ-алгебре другой структуры разделённых степеней на идеал не существует; существующая уникальна.

LaTeX

$$$dividedPowers I = isUnique(I)$$$

Lean4

/-- There are no other divided power structures on an ideal of a  `ℚ`-algebra. -/
theorem dividedPowers_unique (hI : DividedPowers I) : hI = dividedPowers I :=
  hI.ext _
    (fun n x hx ↦ by
      rw [dpow_apply, if_pos hx, eq_comm, inverse_mul_eq_iff_eq_mul _ _ _ (IsUnit.natCast_factorial_of_algebra ℚ n),
        factorial_mul_dpow_eq_pow _ hx])

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