!4#5366

Stream: mathlib4

[Xavier Roblot]

In Data.Matrix.Invertible, mathport translated

/-- A copy of `inv_of_mul_self` using `⬝` not `*`. -/
protected lemma inv_of_mul_self (A : matrix n n α) [invertible A] : ⅟A ⬝ A = 1 := inv_of_mul_self A

into

#print Matrix.invOf_mul_self /-
/-- A copy of `invOf_mul_self` using `⬝` not `*`. -/
protected theorem invOf_mul_self (A : Matrix n n α) [Invertible A] : ⅟ A ⬝ A = 1 :=
  invOf_mul_self A
#align matrix.inv_of_mul_self Matrix.invOf_mul_self
-/

and the same for several other lemmas.

On a quick inspection, these lemmas seem to work fine but I wanted to make sure it was correct.

[Eric Wieser]

It's translating them to comments because they exist already in downstream files

[Eric Wieser]

You should uncomment them and delete the downstream versions

[Eric Wieser]

(which would happen when forward-porting the changes to those downstream files anyway)

[Xavier Roblot]

Oh, I see, #19024 modified also linear_algebra.matrix.nonsingular_inverse, but I only forward-ported the modifications to algebra.invertible. I'll do linear_algebra.matrix.nonsingular_inverse now.

And that has to be done with 4#5366 since it needs Data.Matrix.Invertible.

[Riccardo Brasca]

@Xavier Roblot no need anymore to use "4" to produce links! #5366 should work just fine.

[Eric Wieser]

Just to confirm, it was a good choice to port #5369 separately first; you don't need to edit that PR