ne_of_isReal_isComplex

Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

URI: https://scilib.ai/kg/mathlib#NumberField.InfinitePlace.ne_of_isReal_isComplex

← MathLib Explorer

English

If w is Real and w' is Complex, then w ≠ w'.

Русский

Если w реально, а w' комплексно, то w ≠ w'.

LaTeX

$$$w \\neq w' \\\\text{ whenever } w \\\\text{ real and } w' \\\\text{ complex}.$$$

Lean4

theorem ne_of_isReal_isComplex {w w' : InfinitePlace K} (h : IsReal w) (h' : IsComplex w') : w ≠ w' := fun h_eq ↦
  not_isReal_iff_isComplex.mpr h' (h_eq ▸ h)

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

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

Разделы

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

Аффилиация

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