coe_rangeRestrict

Mathlib.RingTheory.NonUnitalSubring.Basic

URI: https://scilib.ai/kg/mathlib#NonUnitalRingHom.coe_rangeRestrict

English

The product with a left top is equal to the comap of snd: (⊤ : NonUnitalSubring R).prod s = s.comap (NonUnitalRingHom.snd R S).

Русский

Произведение с левой верхней границей равно прообразу проекции snd.

LaTeX

$$$(\top : NonUnitalSubring R).prod s = s.comap (NonUnitalRingHom.snd R S)$$$

Lean4

@[simp]
theorem coe_rangeRestrict (f : R →ₙ+* S) (x : R) : (f.rangeRestrict x : S) = f x :=
  rfl

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

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

Разделы

Аффилиация

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