NF

Mathlib.Tactic.Module

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

Lean4

/-- Basic theoretical "normal form" object of the `match_scalars` and `module` tactics: a type
synonym for a list of ordered pairs in `R × M`, where typically `M` is an `R`-module.  This is the
form to which the tactics reduce module expressions.

(It is not a full "normal form" because the scalars, i.e. `R` components, are not themselves
ring-normalized. But this partial normal form is more convenient for our purposes.) -/
def NF (R : Type*) (M : Type*) :=
  List (R × M)

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

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

Разделы

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

Аффилиация

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