iff_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 \\; \\Longleftrightarrow \\; \\text{Module.Injective } R Q$$$

Lean4

protected theorem iff_injective [Small.{v} R] : Module.Baer R Q ↔ Module.Injective R Q :=
  ⟨Module.Baer.injective, Module.Baer.of_injective⟩

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