bijective_or_eq_zero — Mathlib

English

For simple modules M,N over R, any linear map f: M → N is either bijective or zero.

Русский

Для простых модулей M,N над R любой линейный отображение либо биективно, либо нулево.

LaTeX

$$$[IsSimpleModule(R,M)][IsSimpleModule(R,N)](f: M \\to N)\\; \\text{isBijectiveOrZero}(f).$$$

Lean4

/-- **Schur's Lemma** for linear maps between (possibly distinct) simple modules -/
theorem bijective_or_eq_zero [IsSimpleModule R M] [IsSimpleModule R N] (f : M →ₗ[R] N) : Function.Bijective f ∨ f = 0 :=
  or_iff_not_imp_right.mpr fun h ↦ ⟨injective_of_ne_zero h, surjective_of_ne_zero h⟩

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