logEmbedding_ker — Mathlib

English

The kernel of logEmbedding equals the torsion subgroup, viewed as an additive subgroup.

Русский

Ядро logEmbedding равно торсионной подгруппе, рассматриваемой как аддитивная подгруппа.

LaTeX

$$$\mathrm{ker}(\logEmbedding) = \mathrm{torsion}(K).\text{toAddSubgroup}$$$

Lean4

theorem logEmbedding_ker : (logEmbedding K).ker = (torsion K).toAddSubgroup :=
  by
  ext x
  rw [AddMonoidHom.mem_ker, ← ofMul_toMul x, logEmbedding_eq_zero_iff]
  rfl

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