toSpanSingleton_isIdempotentElem_iff

English

IsIdempotentElem (toSpanSingleton R R e) iff IsIdempotentElem e.

Русский

Будем говорить, что образ спана-единицы идемпотентен тогда и только тогда, когда сам e идемпотентен.

LaTeX

$$$IsIdempotentElem\,(toSpanSingleton\,R\,R\,e) \iff IsIdempotentElem\,e$$$

Lean4

theorem toSpanSingleton_isIdempotentElem_iff {e : R} : IsIdempotentElem (toSpanSingleton R R e) ↔ IsIdempotentElem e :=
  by
  simp_rw [IsIdempotentElem, LinearMap.ext_iff, Module.End.mul_apply, toSpanSingleton_apply, smul_eq_mul, mul_assoc]
  exact ⟨fun h ↦ by conv_rhs => rw [← one_mul e, ← h, one_mul], fun h _ ↦ by rw [h]⟩

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