Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_self_adjoint.star_iff

Modification history

2022-12-14 21:31

src/algebra/star/self_adjoint.lean

feat(algebra/star/basic): add ring_hom.has_involutive_star (#17904) …

Added is_self_adjoint.star_iff View on Github →