rightRigidCategory — Mathlib

English

For a field k and fg modules V,W, the hom set V ⟶ W carries a finite-dimensional k-vector space structure, i.e., the module of linear maps is finite-dimensional.

Русский

Для поля k и fg-модулей V,W множество морфизмов V ⟶ W образует конечномерное пространство над k.

LaTeX

$$∀ (K: Type) [Field K] (V W: FGModuleCat K), Module.Finite K (V ⟶ W)$$

Lean4

instance rightRigidCategory : RightRigidCategory (FGModuleCat K) where

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