mathlib

671d5d9a - feat(algebra/star/self_adjoint): add and generalize trivial lemmas (#18558)

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.