mult_log_place_eq_zero — Mathlib

English

For x ∈ (𝓞 K)ˣ and w ∈ InfinitePlace K, we have mult w · log(w x) = 0 if and only if w x = 1.

Русский

Для x ∈ (𝓞 K)ˣ и w ∈ InfinitePlace(K) выполнено равенство mult w · log(w x) = 0 тогда и только тогда, когда w x = 1.

LaTeX

$$$\bigl\langle \mathrm{mult}(w) \cdot \log(w x) = 0 \bigr\rangle \iff w x = 1$$$

Lean4

theorem mult_log_place_eq_zero {x : (𝓞 K)ˣ} {w : InfinitePlace K} : mult w * Real.log (w x) = 0 ↔ w x = 1 :=
  by
  rw [mul_eq_zero, or_iff_right, Real.log_eq_zero, or_iff_right, or_iff_left]
  · linarith [(apply_nonneg _ _ : 0 ≤ w x)]
  · exact (Units.pos_at_place _ _).ne'
  · exact mult_coe_ne_zero

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