isIdempotentElem_apply_one_iff — Mathlib

English

For f ∈ Module.End R R, IsIdempotentElem (f 1) iff IsIdempotentElem f.

Русский

Для f ∈ Module.End R R верно: идемпотентность f(1) эквивалентна идемпотентности самого f.

LaTeX

$$$IsIdempotentElem (f(1)) \iff IsIdempotentElem f$$$

Lean4

theorem isIdempotentElem_apply_one_iff {f : Module.End R R} : IsIdempotentElem (f 1) ↔ IsIdempotentElem f :=
  by
  rw [IsIdempotentElem, ← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, IsIdempotentElem, LinearMap.ext_iff]
  simp_rw [Module.End.mul_apply]
  exact ⟨fun h r ↦ by rw [← mul_one r, ← smul_eq_mul, map_smul, map_smul, h], (· 1)⟩

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