mem_comap

Mathlib.RingTheory.Valuation.ValuationSubring

URI: https://scilib.ai/kg/mathlib#ValuationSubring.mem_comap

English

Pullback along a composition equals pullback along the composite map.

Русский

Пулбек вдоль композиции равен пулбеку вдоль прямого произведения.

LaTeX

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

Lean4

@[simp]
theorem mem_comap {A : ValuationSubring L} {f : K →+* L} {x : K} : x ∈ A.comap f ↔ f x ∈ A :=
  Iff.rfl

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

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

Разделы

Аффилиация

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