range — Mathlib

English

If a linear map f: M → N has semisimple domain, then the range is semisimple (up to congruence).

Русский

Если область определения линейного отображения полупрямая, то образ отображения полупрямый (через эквивалентность).

LaTeX

$$IsSemisimpleModule R (range f)$$

Lean4

protected theorem range (f : M →ₗ[R] N) : IsSemisimpleModule R (range f) :=
  congr (quotKerEquivRange _).symm

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