unit_smul_eq_iff_mul_eq — Mathlib

English

For a unit u and x in the mixed space, the norm is invariant under the unit smul: ||u • x|| = ||x||.

Русский

Для единицы u и элемента x в смешанном пространстве норма сохраняется: ||u • x|| = ||x||.

LaTeX

$$$\operatorname{norm}(u \cdot x) = \operatorname{norm}(x)$$$

Lean4

theorem unit_smul_eq_iff_mul_eq {x y : 𝓞 K} {u : (𝓞 K)ˣ} : u • mixedEmbedding K x = mixedEmbedding K y ↔ u * x = y :=
  by
  rw [unitSMul_smul, ← map_mul, Function.Injective.eq_iff, ← RingOfIntegers.coe_eq_algebraMap, ← map_mul, ←
    RingOfIntegers.ext_iff]
  exact mixedEmbedding_injective K

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