R

Mathlib.Algebra.Module.Presentation.Tautological

URI: https://scilib.ai/kg/mathlib#Module.Presentation.tautological.R

Lean4

/-- The type which parametrizes the tautological relations in an `A`-module `M`. -/
inductive R
  | add (m₁ m₂ : M)
  | smul (a : A) (m : M)

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

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

Разделы

Аффилиация

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