carrier — Mathlib

English

The carrier type of a finitely generated FGModuleCat object M is the same as the underlying module’s carrier, i.e., the underlying type is M.obj.carrier.

Русский

Тип-носитель объекта FGModuleCat совпадает с носителем модуля: M.carrier = M.obj.carrier.

LaTeX

$$$\\mathrm{FGModuleCat.carrier}(M) = M.obj.carrier$$$

Lean4

/-- A synonym for `M.obj.carrier`, which we can mark with `@[coe]`. -/
def carrier (M : FGModuleCat.{v} R) : Type v :=
  M.obj.carrier

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