feat(LinearAlgebra/Trace): trace-zero idempotent endomorphism over CharZero field is zero

[kim-em]

This PR adds LinearMap.IsIdempotentElem.eq_zero_of_trace_eq_zero: an idempotent endomorphism of a finite-dimensional vector space over a characteristic-zero field with vanishing trace is the zero map.

The proof routes through LinearMap.IsProj.trace (already in this file) — for an idempotent e, the trace equals the rank of range e. Over a CharZero field, vanishing trace forces the rank to zero, hence range e = ⊥ and e = 0.

Extracted from a downstream formalization that needed the lemma to close a Young-symmetrizer off-block-vanishing step, but the statement has no Young / Schur / Specht content — it is a generic CharZero linear-algebra fact.

🤖 Prepared with Claude Code

[github-actions]

PR summary 60a960eb47

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ IsIdempotentElem.eq_zero_of_trace_eq_zero

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.