embedding_mul_absNorm — Mathlib

English

For the height-one spectrum, the sign of the embedding value relates to nonzero-ness of x via a real comparison.

Русский

Значение вложения в спектре высоты единицы связано с ненулевостью x через сравнение на ℝ.

LaTeX

$$0 < ||embedding|| ⇔ x ≠ 0$$

Lean4

theorem embedding_mul_absNorm (v : HeightOneSpectrum (𝓞 K)) {x : 𝓞 (WithVal (v.valuation K))} (h_x_nezero : x ≠ 0) :
    ‖embedding v x‖ * absNorm (v.maxPowDividing (span { x })) = 1 :=
  by
  rw [maxPowDividing, map_pow, Nat.cast_pow, norm_def, adicAbv_def,
    WithZeroMulInt.toNNReal_neg_apply _ ((v.valuation K).ne_zero_iff.mpr (coe_ne_zero_iff.mpr h_x_nezero))]
  push_cast
  rw [← zpow_natCast, ← zpow_add₀ <| mod_cast (zero_lt_one.trans (one_lt_absNorm_nnreal v)).ne']
  norm_cast
  rw [zpow_eq_one_iff_right₀ (Nat.cast_nonneg' _) (mod_cast (one_lt_absNorm_nnreal v).ne')]
  simp [valuation_of_algebraMap, intValuation_if_neg, h_x_nezero]

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