self

Mathlib.LinearAlgebra.FreeModule.Basic

URI: https://scilib.ai/kg/mathlib#Module.Free.self

English

The module structure on R over itself is free.

Русский

Модульная структура над R на R является свободной.

LaTeX

$$$$ \mathrm{Module.Free } R R $$$$

Lean4

/-- The module structure provided by `Semiring.toModule` is free. -/
instance self : Module.Free R R :=
  of_basis (Basis.singleton Unit R)

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

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

Разделы

Аффилиация

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