isConj_symm

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

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

English

IsConj φ σ.symm is equivalent to IsConj φ σ.

Русский

IsConj φ σ.symm эквивалентно IsConj φ σ.

LaTeX

$$IsConj φ σ.symm ↔ IsConj φ σ$$

Lean4

theorem isConj_symm : IsConj φ σ.symm ↔ IsConj φ σ :=
  ⟨IsConj.symm, IsConj.symm⟩

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

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

Разделы

Аффилиация

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