unitCoeff — Mathlib

English

The value of unitCoeff hx equals x multiplied by p raised to the minus its valuation.

Русский

Значение unitCoeff hx равно x, умноженному на p в степени минус его ценности.

LaTeX

$$unitCoeff(hx) = x * p^{(-x.valuation)}$$

Lean4

/-- `unitCoeff hx` is the unit `u` in the unique representation `x = u * p ^ n`.
See `unitCoeff_spec`. -/
def unitCoeff {x : ℤ_[p]} (hx : x ≠ 0) : ℤ_[p]ˣ :=
  let u : ℚ_[p] := x * (p : ℚ_[p]) ^ (-x.valuation : ℤ)
  have hu : ‖u‖ = 1 := by simp [u, hx, pow_ne_zero _ (NeZero.ne _), norm_eq_zpow_neg_valuation]
  mkUnits hu

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