injective_iff_ulift_injective — Mathlib

English

Baer's criterion yields an equivalence: a module Q is Baer if and only if it is injective.

Русский

Критерий Баера даёт эквивалентность: модуль Q является Баеровым тогда и только тогда, когда он инъективен.

LaTeX

$$$ \\text{Baer } R Q \\; \\iff \\; \\text{Module.Injective } R Q$$$

Lean4

theorem injective_iff_ulift_injective : Module.Injective R M ↔ Module.Injective R (ULift.{v'} M) :=
  ⟨Module.ulift_injective_of_injective R, Module.injective_of_ulift_injective R⟩

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