idemFst_compl — Mathlib

English

The sum of the two projections equals the identity endomorphism: idemFst + idemSnd = 1 on WithLp p (α × β).

Русский

Сумма двух проекций равна тождественному концу на WithLp p (α × β).

LaTeX

$$$\\mathrm{idemFst} + \\mathrm{idemSnd} = 1_{\\mathrm{End}(WithLp\\ p\\ (\\alpha \\times \\beta))}$$$

Lean4

theorem idemFst_compl : (1 : AddMonoid.End (WithLp p (α × β))) - idemFst = idemSnd := by
  rw [← idemFst_add_idemSnd, add_sub_cancel_left]

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