self_adjoint): generalize a lemma to `semifield` (#18687)

Commit

2 years ago

chore(algebra/star/self_adjoint): generalize a lemma to `semifield` (#18687) This was missed in a previous commit, and backports a change made during forward-porting.

Author

eric-wieser

Parents

91862a60

mathlib a6ece354 - chore(algebra/star/self_adjoint): generalize a lemma to `semifield` (#18687)

mathlib
a6ece354 - chore(algebra/star/self_adjoint): generalize a lemma to `semifield` (#18687)