selfZPow_of_nonneg — Mathlib

English

In a localization setting with irreducible x, there exists a representation of any nonzero b ∈ B as a product of a power of selfZPow and an image of a in R, with certain non-divisibility conditions.

Русский

При локализации и неудалимой x существует представление любого ненулевого b ∈ B как произведения степени самопозиционного элемента и образа элемента a из R с дополнительными условиями неверного деления.

LaTeX

$$$\exists a\in R,\ n\in \mathbb{Z},\ b = selfZPow(x,B,n) \cdot algebraMap(R,B)(a)$$$

Lean4

theorem selfZPow_of_nonneg {n : ℤ} (hn : 0 ≤ n) : selfZPow x B n = algebraMap R B x ^ n.natAbs :=
  dif_pos hn

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