complexEmbedding_apply

Mathlib.NumberTheory.NumberField.Units.Basic

URI: https://scilib.ai/kg/mathlib#NumberField.Units.complexEmbedding_apply

English

Applying a complex embedding to a unit yields the expected image under φ.

Русский

Применение комплексного вложения к единице даёт ожидаемое изображение под φ.

LaTeX

$$@[simp] complexEmbedding_apply (φ) (u) : Units.complexEmbedding φ u = φ u$$

Lean4

@[simp]
protected theorem complexEmbedding_apply (φ : K →+* ℂ) (u : (𝓞 K)ˣ) : Units.complexEmbedding φ u = φ u :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru