of_isComplemented_domain — Mathlib

English

If m is a complemented submodule of M, then the space of linear maps from m to P is finite over R₀.

Русский

Если m — дополненный подмодуль M, то множество линейных отображений m → P является конечномерным по отношению к R₀.

LaTeX

$$IsComplemented m → Module.Finite R₀ (m →ₗ[R] P)$$

Lean4

theorem of_isComplemented_domain (h : IsComplemented m) : Module.Finite R₀ (m →ₗ[R] P) :=
  .of_surjective (.lcomp R₀ P ..) (LinearMap.surjective_comp_subtype_of_isComplemented h)

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