Matrix.IsSymm for inverses

Stream: Is there code for X?

[Edison Xie]

Do we have something like this in Mathlib?

import Mathlib

open Matrix in
lemma Matrix.IsSymm.inv {n R : Type*} [DecidableEq n] [Fintype n] [CommRing R] {A : Matrix n n R}
    (hA : A.IsSymm) : A⁻¹.IsSymm := by
  if hA' : IsUnit A.det then
  haveI : Invertible A := invertibleOfIsUnitDet A hA'
  rw [IsSymm, ← mul_one A⁻¹ᵀ, ← mul_inv_cancel_right_of_invertible A 1, one_mul, ← mul_assoc]
  nth_rw 2 [← hA.eq]
  rw [← transpose_mul, ← mul_one (A * A⁻¹), mul_assoc, mul_inv_cancel_left_of_invertible]
  simp
  else
  simp [Matrix.inv, Ring.inverse, hA']

[Edison Xie]

@Eric Wieser

[Ruben Van de Velde]

Doesn't look like it

[Ruben Van de Velde]

import Mathlib

lemma Matrix.IsSymm.adjugate {n R : Type*} [DecidableEq n] [Fintype n] [CommRing R] {A : Matrix n n R}
    (hA : A.IsSymm) : A.adjugate.IsSymm := by
  rw [IsSymm, Matrix.adjugate_transpose, hA.eq]

open Matrix in
lemma Matrix.IsSymm.inv {n R : Type*} [DecidableEq n] [Fintype n] [CommRing R] {A : Matrix n n R}
    (hA : A.IsSymm) : A⁻¹.IsSymm := by
  rw [Matrix.inv_def]
  exact hA.adjugate.smul _

[Eric Wieser]

Those can both be Iffs, right?

[Eric Wieser]

Do we have docs#Matrix.IsHermitian.inv ?

[Damiano Testa]

Are those matrices expected to be invertible? A low rank matrix will have adjugate equal to 0, right?

[Damiano Testa]

If that is the case, then those are not iffs.

[Damiano Testa]

Ok, here is an example of a non-symmetric matrix whose adjugate is symmetric:

import Mathlib

abbrev M := !![(0 : ℤ), 1, 0; 0, 0, 0; 0, 0, 0]

example : M.adjugate.IsSymm := by decide
example : ¬ M.IsSymm := by decide

[Ruben Van de Velde]

#33748