Every change of #8291 is also updated into #8289.
If #8289 is approved first, then this PR will be redundant.

I don't recommend this strategy - please focus on this PR first. Large PRs are harder to review, especially if they do lots of unrelated things.

@eric-wieser, I thought what you mentioned are several blocks of lemmas. As they are just single lemmas, I think I can do them today.

That's great news! Having looked again, the two update_* lemmas need the pi.has_star instance that you had difficulty with before, so let's not bother with those two in this PR.

The other two has been added! @eric-wieser
I think the solution for the other PR is, if some new definitions seem should be in new files, then just remove them. I didn't give any lemma to one or two defs anyway.

I have another pending PR #8289 contributing to this file as well.

That's fine, git will handle unifying the two for us. Once this one is merged into master, I can help you merge the changes into your other PR.

Are you happy with the addition to the authors list?

Yes! I care very little about determining who counts as an "author" of a file. If you contribute to a file and would like credit for it, go for it, I would say.

Build failed (retrying...):

• Build mathlib

@eric-wieser Eric, an issue unrelated to the file changed seems to have arisen.

Don't worry. Bors should automatically figure out which commit is causing the issue, and merge all the correct commits.

@eric-wieser

@[simp] lemma conj_transpose_one [decidable_eq n] [semiring α] [star_ring α]:
  (1 : matrix n n α)ᴴ = 1 :=
by simp [conj_transpose]

This is very amazing to me. How can I know which lemmas simp used?

You can replace simp with simp? and it will tell you what lemmas it used

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests