feat(linear_algebra/matrix/nonsingular_inverse.lean): more lemmas

[l534zhan]

added some lemmas connecting some existing lemmas. More convenient for end-users.

---

• depends on: [Merged by Bors] - feat(linear_algebra/nonsingular_inverse): add lemmas about invertible #8201

[eric-wieser]

I don't think this defintion (which the linter will tell you should be a def not a lemma) is a particularly good idea invertible is usually reserved for instances, and is_unit is for everything else:

Suggested change

	/-- Matrix A is invertible implies `det A` is a unit. -/
	noncomputable
	lemma invertible_of_is_unit_det (h : is_unit A.det) : invertible A :=
	⟨A⁻¹, nonsing_inv_mul A h, mul_nonsing_inv A h⟩
	/-- Matrix A is invertible implies `det A` is a unit. -/
	lemma is_unit_of_is_unit_det (h : is_unit A.det) : is_unit A :=
	sorry

[l534zhan]

Hi, Eric. The thing you pointed out is very reasonable. The suggested lemma "is_unit_of_is_unit_det" has already existed in the file, but it won't be very helpful for proving other lemmas followed. I wrote "invertible_of_is_unit_det" as it will then be used to prove other newly added lemmas such as B is right invertible implies B is the inverse (I didn't see another quick way to establishing this other than adding "invertible_of_is_unit_det"). Perhaps just change the lemmas the linter pointed out to definitions and put comments like "an end-user should usually not use this" beside them if necessary?
(If we have h : is_unit A.det, then we can then indeed construct an instance of invertible A. From this point of view, something like "invertible_of_is_unit_det" may be worth adding.)

[l534zhan]

How about changing "invertible_of_is_unit_det" to def and deleting "invertible_of_left_inverse" and "invertible_of_right_inverse" both together as the two may seem unnecessary (or change them to def as well)?

[l534zhan]

If the "def" invertible_of_is_unit_det still seems improper for users to use outside the file, perhaps use private def?

[eric-wieser]

The whole point of invertible is to be a computable version of is_unit. This def is noncomputable which completely defeats that point.

[pechersky]

What is the norm attribute?

[l534zhan]

I don't fully understand norm actually. Perhaps delete it?

[eric-wieser]

Reviewing this is making me realize we're missing some rather basic api for invertible (#8195).

I've a PR in the works that adds:

/-- If `A.det` has a constructive inverse, produce one for `A`. -/
def invertible_of_det_invertible [invertible A.det] : invertible A :=
{ inv_of := ⅟A.det • A.adjugate,
  mul_inv_of_self := by rw [
    mul_smul_comm, matrix.mul_eq_mul, mul_adjugate, smul_smul, inv_of_mul_self, one_smul],
  inv_of_mul_self := by rw [
    smul_mul_assoc, matrix.mul_eq_mul, adjugate_mul, smul_smul, inv_of_mul_self, one_smul] }

/-- If `A` has a constructive inverse, produce one for `A.det`. -/
def det_invertible_of_invertible [invertible A] : invertible A.det :=
{ inv_of := by exactI det (⅟A),
  inv_of_mul_self := by rw [←det_mul, ←matrix.mul_eq_mul, inv_of_mul_self, det_one],
  mul_inv_of_self := by rw [←det_mul, ←matrix.mul_eq_mul, mul_inv_of_self, det_one] }

which I think makes most of these new lemmas trivial.

[eric-wieser]

In case it helps, a summary of the different indicators of unitness are as follows:

• is_unit a - I need a to have an inverse and I don't care what it is or need to compute it
• invertible a - I need a to have an inverse and I need to compute it
• units A - I need some object and its associated inverse together

Often invertible is the strongest statement, and all the other versions can be derived from it.

[l534zhan]

Great, Eric! Your contribution will improve some of the proofs I used. As the PR is ready to merge (perhaps after deleting norm).
How about approving this PR first and improving the proofs later in a new PR after your contribution has been merged?
@eric-wieser

[eric-wieser]

No, I think we should wait for that PR to go through and then change things to use invertible_of_det_invertible etc before merging this PR. Lemmas which conclude is_unit from invertible aren't useful (apart from is_unit_of_invertible) - you should either conclude invertible from invertible or is_unit from is_unit.

[l534zhan]

@eric-wieser I think yours has been merged. I will change the things here then. Is #8195 the only relevant PR you made?

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - feat(linear_algebra/nonsingular_inverse): add lemmas about invertible #8201

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!