exists_isRegular_of_finrank_le_card

English

If finrank_R M ≤ #R, then there exists x ∈ L such that IsRegular R M x.

Русский

Если финальный ранг R-модуля M не превышает размер R, то существует x ∈ L такой, что IsRegular R M x.

LaTeX

$$$$ \\exists x : L, \\; \\operatorname{IsRegular} R M x $$$$

Lean4

theorem exists_isRegular_of_finrank_le_card (h : finrank R M ≤ #R) : ∃ x : L, IsRegular R M x :=
  LinearMap.exists_isNilRegular_of_finrank_le_card _ h

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