Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_self_adjoint_add_star_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_add_star_self View on Github →