logEmbedding_eq_zero_iff — Mathlib

English

logEmbedding K (Additive.ofMul x) = 0 if and only if x ∈ torsion K.

Русский

logEmbedding K (Additive.ofMul x) = 0 тогда и только тогда, когда x ∈ torsion K.

LaTeX

$$$\logEmbedding K (Additive.ofMul x) = 0 \iff x \in \mathrm{torsion}(K)$$$

Lean4

theorem logEmbedding_eq_zero_iff {x : (𝓞 K)ˣ} : logEmbedding K (Additive.ofMul x) = 0 ↔ x ∈ torsion K :=
  by
  rw [mem_torsion]
  refine ⟨fun h w ↦ ?_, fun h ↦ ?_⟩
  · by_cases hw : w = w₀
    · suffices -mult w₀ * Real.log (w₀ (x : K)) = 0
        by
        rw [neg_mul, neg_eq_zero, ← hw] at this
        exact mult_log_place_eq_zero.mp this
      rw [← sum_logEmbedding_component, sum_eq_zero]
      exact fun w _ ↦ congrFun h w
    · exact mult_log_place_eq_zero.mp (congrFun h ⟨w, hw⟩)
  · ext w
    rw [logEmbedding_component, h w.val, Real.log_one, mul_zero, Pi.zero_apply]

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