codRestrict

Mathlib.RingTheory.NonUnitalSubsemiring.Defs

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

Lean4

/-- Restriction of a non-unital ring homomorphism to a non-unital subsemiring of the codomain. -/
def codRestrict (f : F) (s : S') (h : ∀ x, f x ∈ s) : R →ₙ+* s
    where
  toFun n := ⟨f n, h n⟩
  map_mul' x y := Subtype.eq (map_mul f x y)
  map_add' x y := Subtype.eq (map_add f x y)
  map_zero' := Subtype.eq (map_zero f)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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