rank_self — Mathlib

English

For any ring R satisfying strong rank condition, the rank of R as an R-module over itself equals 1.

Русский

Для кольца R, удовлетворяющего условию сильной ранговости, ранг R как модуля над самим R равен 1.

LaTeX

$$\\operatorname{rank}_R(R) = 1$$

Lean4

@[simp]
theorem rank_self : Module.rank R R = 1 := by
  rw [← Cardinal.lift_inj, ← (Basis.singleton PUnit R).mk_eq_rank, Cardinal.mk_punit]

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