of_subsingleton — Mathlib

English

If N is a Subsingleton, then N is free as an R-module.

Русский

Если N — пододносное множество, то N свободно как R-модуль.

LaTeX

$$$$ [Subsingleton\ N] \Rightarrow \mathrm{Module.Free } R N $$$$

Lean4

instance (priority := 100) of_subsingleton [Subsingleton N] : Module.Free R N :=
  of_basis.{u, z, z}
    (Basis.empty N : Basis PEmpty R N)
      -- This was previously a global instance,
      -- but it doesn't appear to be used and has been implicated in slow typeclass resolutions.

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