rank_linearMap_self — Mathlib

English

If S is a module over R with appropriate freeness, then the rank formula holds for self-maps.

Русский

При наличии надлежащей свободы ранговая формула верна и для самих отображений.

LaTeX

$$$$ \mathrm{rank}_S(\mathrm{Hom}_R(M, S)) = \mathrm{rank}_R M $$$$

Lean4

theorem rank_linearMap_self : Module.rank S (M →ₗ[R] S) = lift.{u'} (Module.rank R M) := by
  rw [rank_linearMap, rank_self, lift_one, mul_one]

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