isIdempotentElem_inr_iff — Mathlib

English

Idempotence is preserved under inr embedding into the unitization.

Русский

Идempotентность сохраняется при вложении inr в единичизацию.

LaTeX

$$IsIdempotentElem (inr a) ⇔ IsIdempotentElem a$$

Lean4

@[simp]
theorem isIdempotentElem_inr_iff (R : Type*) {A : Type*} [MulZeroClass R] [AddZeroClass A] [Mul A] [SMulWithZero R A]
    {a : A} : IsIdempotentElem (a : Unitization R A) ↔ IsIdempotentElem a := by
  simp only [IsIdempotentElem, ← inr_mul, inr_injective.eq_iff]

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