dpow — Mathlib

English

Compatibility lemmas ensure that various proofs of dpow on quotient map to dpow on the original via f.

Русский

Леммы совместимости обеспечивают, что различные доказательства dpow на факторе соответствуют dpow на оригинале через f.

LaTeX

$$$dpow\\_apply'\\,(hIf)\\ (ha) : dpow(hI,f,n)(f(a)) = f(hI.dpow(n,a))$$$

Lean4

/-- The definition of divided powers on `A ⧸ J`. Tagged as noncomputable because it makes use of
  `Function.extend`, but under `IsSubDPIdeal hI (J ⊓ I)`, `dividedPowers_unique` proves that no
  choices are involved. -/
noncomputable def dpow (J : Ideal A) : ℕ → A ⧸ J → A ⧸ J :=
  DividedPowers.Quotient.OfSurjective.dpow hI (Ideal.Quotient.mk J)

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