nonUnitalRingHom

Mathlib.Algebra.Ring.Pi

URI: https://scilib.ai/kg/mathlib#Pi.nonUnitalRingHom

Lean4

/-- A family of non-unital ring homomorphisms `f a : γ →ₙ+* β a` defines a non-unital ring
homomorphism `Pi.nonUnitalRingHom f : γ →+* Π a, β a` given by
`Pi.nonUnitalRingHom f x b = f b x`. -/
@[simps]
protected def nonUnitalRingHom {γ : Type w} [∀ i, NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ]
    (g : ∀ i, γ →ₙ+* f i) : γ →ₙ+* ∀ i, f i :=
  { Pi.mulHom fun i => (g i).toMulHom, Pi.addMonoidHom fun i => (g i).toAddMonoidHom with toFun := fun x b => g b x }

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

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

Разделы

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

Аффилиация

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