diagram — Mathlib

English

An abbreviation for S.fintypeDiagram followed by the functor to Profinite.

Русский

Сокращение для S.fintypeDiagram последовательности композиции со светлым Profinite.

LaTeX

$$$\\operatorname{diagram} \\; S = S.fintypeDiagram \\; \\circ\\; FintypeCat.toLightProfinite$$$

Lean4

/-- An abbreviation for `S.fintypeDiagram ⋙ FintypeCat.toProfinite`. -/
abbrev diagram : ℕᵒᵖ ⥤ LightProfinite :=
  S.fintypeDiagram ⋙ FintypeCat.toLightProfinite

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