isReal_smul_iff

Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

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

English

IsReal is preserved under smul: IsReal(σ • w) iff IsReal(w).

Русский

Real-свойство сохраняется при действии: IsReal(σ • w) эквивалично IsReal(w).

LaTeX

$$$ \mathrm{IsReal}(\sigma \cdot w) \iff \mathrm{IsReal}(w) $$$

Lean4

theorem isReal_smul_iff : IsReal (σ • w) ↔ IsReal w :=
  isReal_comap_iff (f := σ.symm.toRingEquiv)

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

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

Разделы

Аффилиация

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