[Merged by Bors] - feat: make rank_mul_eq_left_of_isUnit_det into an effective simp lemma

[JonBannon]

These theorems give that if A is a unit, or a unitary, in the n x n matrices over a commutative ring R, and B is an m x n matrix over R, that multiplying B by A on the left or right doesn't change the rank of B. To facilitate this, added isUnits_det_units and det_isUnit lemmas.

---

[eric-wieser]

I'm a little sad that this API has to exist. The problem seems to be that we don't have a standard way to talk about whether a matrix is invertible, and so we end up writing lemmas for every possible way we might want to write it (IsUnit M, IsUnit M.det, M : Units (Matrix _ _ _), Invertible M).

If we declared IsUnit M the simp-normal form of IsUnit M.det (or possibly vice-versa), then we could mark Units.isUnit simp and we probably wouldn't need these new lemmas.

[j-loreaux]

How would simp actually apply the IsUnit version? I didn't think this problem is specific to matrices at all.

[eric-wieser]

How would simp actually apply the IsUnit version?

simp would automatically solve any side-goals of the form IsUnit (Units.val u), since the unit-ness is structural.

[j-loreaux]

@eric-wieser ha! I didn't know that worked. This wasn't available in Lean 3, was it?

I think in the Matrix library we phrase things in terms of IsUnit (det A) instead of IsUnit A almost all the time. At the same time, I don't think we actually want Matrix.isUnit_iff_isUnit_det to be a simp lemma.

One thing we could do: mark rank_mul_eq_right_of_isUnit_det and similar as @[simp], and then add simp lemmas, which then allow these to trigger.

import Mathlib

-- some hypotheses too strong maybe
variable {m n R : Type*} [Fintype n] [CommRing R] [StarRing R] [DecidableEq n]
namespace Matrix

@[simp]
lemma isUnit_det_units (A : (Matrix n n R)ˣ) : IsUnit (det (A : Matrix n n R)) :=
  A.isUnit.map detMonoidHom

@[simp]
lemma isUnit_det_unitaryGroup (A : unitaryGroup n R) : IsUnit (det (A : Matrix n n R)) :=
  (unitary.toUnits A).isUnit.map detMonoidHom

attribute [simp] rank_mul_eq_left_of_isUnit_det rank_mul_eq_right_of_isUnit_det
  isUnit_det_of_invertible

-- then the following work `by simp`

theorem rank_mul_unitary (A : unitaryGroup n R) (B : Matrix m n R) :
    rank (B * (A : Matrix n n R)) = rank B := by
  simp? -- simp only [isUnit_det_unitaryGroup, rank_mul_eq_left_of_isUnit_det]

theorem rank_unitary_mul [Fintype m] (A : unitaryGroup n R)
    (B : Matrix n m R) : rank ((A : Matrix n n R) * B) = rank B := by
  simp? -- simp only [isUnit_det_unitaryGroup, rank_mul_eq_right_of_isUnit_det]

end Matrix

[j-loreaux]

@eric-wieser I've implemented the change I posted above. Even if we decide that we want to refactor the matrix library and how we handle invertibility, it shouldn't be part of this PR. But now I've rewritten the content of this PR, so I shouldn't merge it.

[eric-wieser]

!bench

[eric-wieser]

Thanks, this looks good now. Let's check there's no major performance regression.

Can you check the PR description is up to date with the new version?

bors d+

[mathlib-bors]

✌️ JonBannon can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[leanprover-bot]

Here are the benchmark results for commit a3f60b1.
There were no significant changes against commit e8433a6.

[JonBannon]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style