top_prod

Mathlib.Algebra.Ring.Subsemiring.Basic

URI: https://scilib.ai/kg/mathlib#Subsemiring.top_prod

English

For any s ⊆ R, the product ⊤.prod s equals s.comap (snd R S), i.e., the second projection pullback.

Русский

Для любого s ⊆ R верно: ⊤.prod s = s.comap (snd R S).

LaTeX

$$$\\top\\prod s = s.comap(\\text{RingHom.snd } R S)$$$

Lean4

theorem top_prod (s : Subsemiring S) : (⊤ : Subsemiring R).prod s = s.comap (RingHom.snd R S) :=
  ext fun x => by simp [mem_prod]

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

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

Разделы

Аффилиация

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