English
Any Noetherian ring satisfies Orzech's property, i.e., certain lifting/injectivity properties hold for submodules and maps.
Русский
Любое Нётерово кольцо удовлетворяет свойству Ореча: выполняются определенные свойства переноса(инъектности) для подмодулей и отображений.
LaTeX
$$$\\text{OrzechProperty } R$ for every Noetherian ring $R$$$
Lean4
/-- Any Noetherian ring satisfies Orzech property.
See also `IsNoetherian.injective_of_surjective_of_submodule` and
`IsNoetherian.injective_of_surjective_of_injective`. -/
instance (priority := 100) orzechProperty (R) [Ring R] [IsNoetherianRing R] : OrzechProperty R where
injective_of_surjective_of_submodule'
{M} :=
letI := Module.addCommMonoidToAddCommGroup R (M := M)
IsNoetherian.injective_of_surjective_of_submodule
