comap_smul

Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

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

English

Pulling back after a smul corresponds to smul after pulling back along the inverse automorphism.

Русский

Обратное после действия соответствует действию после обратного автоморфизма.

LaTeX

$$$ (\sigma \cdot w).\mathrm{comap} f = w.\mathrm{comap}( (\sigma^{-1}) \circ f ) $$$

Lean4

theorem comap_smul {f : F →+* K} : (σ • w).comap f = w.comap (RingHom.comp σ.symm f) :=
  rfl

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

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

Разделы

Аффилиация

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