map — Mathlib

English

The image of an orthogonal idempotent family under a ring hom is again an orthogonal idempotent family.

Русский

Образ семейства ортогональных идемпотентов под гомоморфизм кольца снова является семейством ортогональных идемпотентов.

LaTeX

$$OrthogonalIdempotents (f ∘ e)$$

Lean4

theorem map (he : OrthogonalIdempotents e) : OrthogonalIdempotents (f ∘ e) := by
  classical simp [iff_mul_eq, he.mul_eq, ← map_mul f, apply_ite f]

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