algebraMap

Mathlib.Tactic.Module

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Module.NF.algebraMap

Lean4

/-- Operate on a `Module.NF S M` object `l`, i.e. a list of pairs in `S × M`, where `S` is some
commutative semiring, by applying to each `S`-component the algebra-map from `S` into a specified
`S`-algebra `R`. -/
def algebraMap [CommSemiring S] [Semiring R] [Algebra S R] (l : NF S M) : NF R M :=
  l.map (fun ⟨s, x⟩ ↦ (_root_.algebraMap S R s, x))

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

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

Разделы

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

Аффилиация

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