rank_le_of_surjective — Mathlib

English

If f: M ≃_R M' is a linear equivalence, then the dimensions of M and M' are equal.

Русский

Если существует линейное эквивалентное отображение f: M ≃_R M', то размерности M и M' равны.

LaTeX

$$$\operatorname{Module.rank} R M = \operatorname{Module.rank} R M'$$$

Lean4

theorem rank_le_of_surjective (f : M →ₗ[R] M₁) (h : Surjective f) : Module.rank R M₁ ≤ Module.rank R M :=
  by
  rw [← rank_range_of_surjective f h]
  apply rank_range_le

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