self_adjoint): remove commutativity hypothesis from `has_pow (self_adjoint R)` (#12188)

Commit

4 years ago

feat(algebra/star/self_adjoint): remove commutativity hypothesis from `has_pow (self_adjoint R)` (#12188) This was put in the wrong section. Powers of selfadjoint elements are still selfadjoint.

Author

j-loreaux

Parents

a6078202

mathlib3 2971f3dc - feat(algebra/star/self_adjoint): remove commutativity hypothesis from `has_pow (self_adjoint R)` (#12188)

mathlib3
2971f3dc - feat(algebra/star/self_adjoint): remove commutativity hypothesis from `has_pow (self_adjoint R)` (#12188)