Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-17 00:34 84f12be1

View on Github →

chore(algebra/star/self_adjoint): improve definitional unfolding of pow and div (#12085)

Estimated changes

added theorem self_adjoint.coe_div
modified theorem self_adjoint.coe_inv
modified theorem self_adjoint.coe_mul
modified theorem self_adjoint.coe_one
added theorem self_adjoint.coe_pow
added theorem self_adjoint.coe_zpow