isIntegral — Mathlib

English

If M is a finite R-module, then the endomorphism ring End_R(M) is integral over R.

Русский

Если M конечно как R-модуль, то кольцо концевых отображений End_R(M) интегрально над R.

LaTeX

$$$\text{If } M\text{ is finite over }R,\; \mathrm{End}_R(M)\text{ is integral over }R.$$$

Lean4

instance isIntegral {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M] :
    Algebra.IsIntegral R (Module.End R M) :=
  ⟨LinearMap.exists_monic_and_aeval_eq_zero R⟩

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