comap_comp

Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

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

English

Pulling back along a composition f ∘ g is the same as pulling back first along f and then along g.

Русский

Обратное по композиции f ∘ g равно обратному по f, затем по g.

LaTeX

$$$ w.\mathrm{comap}(f \circ g) = (w.\mathrm{comap} f).\mathrm{comap} g $$$

Lean4

theorem comap_comp (w : InfinitePlace K) (f : F →+* K) (g : k →+* F) : w.comap (f.comp g) = (w.comap f).comap g :=
  rfl

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

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

Разделы

Аффилиация

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