orderOf_isConj_two_of_ne_one

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

URI: https://scilib.ai/kg/mathlib#NumberField.ComplexEmbedding.orderOf_isConj_two_of_ne_one

← MathLib Explorer

English

If hσ: IsConj φ σ and σ ≠ 1, then order(σ) = 2.

Русский

Если hσ: IsConj φ σ и σ ≠ 1, то порядок σ равен 2.

LaTeX

$$IsConj φ σ ∧ σ ≠ 1 → orderOf σ = 2$$

Lean4

theorem orderOf_isConj_two_of_ne_one (hσ : IsConj φ σ) (hσ' : σ ≠ 1) : orderOf σ = 2 :=
  orderOf_eq_prime_iff.mpr ⟨by ext; simpa using isConj_apply_apply hσ _, hσ'⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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