Commit 2023-03-08 13:45 671d5d9a

feat(algebra/star/self_adjoint): add and generalize trivial lemmas (#18558) This:

• Generalizes is_self_adjoint.smul, which makes it easier to show that 0.5 • x is self-adjoint when x is, even if 0.5 is a complex number.
• Generalizes is_self_adjoint.add to match matrix.is_hermitian.add (for a later refactor), along with many other lemmas.
• Removes re-proofs of star_nat_cast and star_int_cast. The first is motivated by showing that exp K m for some matrix m is positive definite if is_self_adjoint m. Forward-ported at https://github.com/leanprover-community/mathlib4/pull/2719.