map_logEmbedding_sup_torsion — Mathlib

English

For a subgrp s of logSpace(K), the image of s ⊔ torsion under logEmbedding equals the image of s.

Русский

Для подгруппы s в logSpace(K) образ s ⊔ torsion под logEmbedding равен образу s.

LaTeX

$$$\mathrm{map}(\logEmbedding K)(s \sqcup \mathrm{torsion}(K)) = \mathrm{map}(\logEmbedding K)(s)$$$

Lean4

theorem map_logEmbedding_sup_torsion (s : AddSubgroup (Additive (𝓞 K)ˣ)) :
    (s ⊔ (torsion K).toAddSubgroup).map (logEmbedding K) = s.map (logEmbedding K) := by
  rw [← logEmbedding_ker, AddSubgroup.map_eq_map_iff, sup_right_idem]

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