complexEmbedding_inj — Mathlib

English

The complex embedding is injective on the unit group as a map to ℂ.

Русский

Комплексное вложение инъективно на множестве единиц, отображаемом в ℂ.

LaTeX

$$Injective (NumberField.Units.complexEmbedding φ)$$

Lean4

@[simp]
protected theorem complexEmbedding_inj (φ : K →+* ℂ) (u v : (𝓞 K)ˣ) :
    Units.complexEmbedding φ u = Units.complexEmbedding φ v ↔ u = v :=
  (Units.complexEmbedding_injective φ).eq_iff

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