torsion_smul_mem_of_mem — Mathlib

English

If x is in the fundamental cone and ζ is a torsion unit, then ζ · x remains in the fundamental cone.

Русский

Если x в фундаментальном конусе и ζ — тorsion единица, то ζ·x остаётся в фундаментальном конусе.

LaTeX

$$(hx : x ∈ fundamentalCone(K)) (hζ : ζ ∈ torsion K) ⇒ ζ·x ∈ fundamentalCone(K).$$

Lean4

theorem torsion_smul_mem_of_mem (hx : x ∈ fundamentalCone K) {ζ : (𝓞 K)ˣ} (hζ : ζ ∈ torsion K) :
    ζ • x ∈ fundamentalCone K := by
  constructor
  · rw [Set.mem_preimage, logMap_torsion_smul _ hζ]
    exact hx.1
  · rw [Set.mem_setOf_eq, unitSMul_smul, map_mul, norm_unit, one_mul]
    exact hx.2

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