Diagonals of symmetric idempotent matrices

A symmetric idempotent matrix P — an orthogonal projector — satisfies P = PᵀP, so each diagonal entry is a sum of squares, P i i = ∑ j, P i j ^ 2, and over an ordered ring lies in [0, 1].

[UPSTREAM] candidate.

theorem Matrix.diag_eq_sum_sq_of_isSymm_of_isIdempotentElem {n : Type u_1} {R : Type u_2} [Fintype n] [CommSemiring R] {P : Matrix n n R} (hs : P.IsSymm) (hp : IsIdempotentElem P) (i : n) : P i i = ∑ j : n, P i j ^ 2

theorem Matrix.diag_nonneg_of_isSymm_of_isIdempotentElem {n : Type u_1} {R : Type u_2} [Fintype n] [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {P : Matrix n n R} (hs : P.IsSymm) (hp : IsIdempotentElem P) (i : n) : 0 ≤ P i i

theorem Matrix.diag_le_one_of_isSymm_of_isIdempotentElem {n : Type u_1} {R : Type u_2} [Fintype n] [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {P : Matrix n n R} (hs : P.IsSymm) (hp : IsIdempotentElem P) (i : n) : P i i ≤ 1