mulSingle

Mathlib.Algebra.Group.Pi.Lemmas

URI: https://scilib.ai/kg/mathlib#OneHom.mulSingle

Lean4

/-- The one-preserving homomorphism including a single value
into a dependent family of values, as functions supported at a point.

This is the `OneHom` version of `Pi.mulSingle`. -/
@[to_additive /-- The zero-preserving homomorphism including a single value into a dependent family of values,
      as functions supported at a point.

      This is the `ZeroHom` version of `Pi.single`. -/
    ]
nonrec def mulSingle [∀ i, One <| f i] (i : I) : OneHom (f i) (∀ i, f i)
    where
  toFun := mulSingle i
  map_one' := mulSingle_one i

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

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

Разделы

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

Аффилиация

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