Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_self_adjoint_star_add_self

Modification history

2023-03-19 20:21
src/algebra/star/self_adjoint.lean
refactor(linear_algebra/matrix/hermitian): golf and generalize (#18565) …
Added is_self_adjoint_star_add_selfView on Github →