ker_toSpanSingleton_one_sub_eq_span

English

Let e be an idempotent element in a commutative ring R. Then the kernel of the linear map toSpanSingleton(R, R, 1 - e) is the principal ideal generated by e.

Русский

Пусть e — идемпотентный элемент в коммутативном кольце R. Тогда ядро линейного отображения toSpanSingleton(R, R, 1 − e) равно главному идеалу, порожденному e.

LaTeX

$$$\ker\big(\mathrm{toSpanSingleton}(R,R,1 - e)\big) = \langle e \rangle$$$

Lean4

theorem ker_toSpanSingleton_one_sub_eq_span :
    LinearMap.ker (LinearMap.toSpanSingleton R R (1 - e)) = Ideal.span { e } := by
  rw [ker_toSpanSingleton_eq_span he.one_sub, sub_sub_cancel]

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