how can i show lean it's inv??!

Stream: new members

[Hbz]

import Mathlib

open Matrix Polynomial

noncomputable section

variable (R : Type*) [Field R]

def givenCharPoly : Polynomial R := (X - 2)^2 * (X + 1)

def Matrix3x3 := Matrix (Fin 3) (Fin 3) R

#check Matrix3x3 R

instance : CommRing R := by
exact Field.toCommRing

def F_A : Matrix3x3 R:=
  !![
    (0:R), (0:R), (-2:R);
    (1:R), (0:R), (-5:R);
    (0:R), (1:R), (-4:R)]
#check F_A

#check (F_A R).charpoly
#check givenCharPoly

lemma F_A_charPoly : (F_A R).charpoly = givenCharPoly R := by

  sorry

example (A : Matrix3x3 R) (h : A.charpoly = givenCharPoly R) :
  ∃ P : Matrix3x3 R, P⁻¹ * A * P = F_A := by

lean show me that the P⁻¹ * A * P
failed to synthesize
Inv (Matrix3x3 R)
so how can i correct this,thank you!!!

[Etienne Marion]

Does it work if you make Matrix3x3 an abbrev instead? (i.e. replace def with abbrev)

[Hbz]

thank you.
andi have another question.

import Mathlib

open Matrix Polynomial

noncomputable section

variable {R : Type*} [Field R]

def givenCharPoly : Polynomial R := (X - 2)^2 * (X + 1)

abbrev Matrix3x3 := Matrix (Fin 3) (Fin 3) R

#check Matrix3x3

instance : CommRing R := by
exact Field.toCommRing

def F_A : Matrix3x3:=
  !![
    (0:R), (0:R), (-2:R);
    (1:R), (0:R), (-5:R);
    (0:R), (1:R), (-4:R)]
#check F_A

#check (F_A).charpoly
#check givenCharPoly

lemma F_A_charPoly : (F_A).charpoly = givenCharPoly := by

  sorry

example (A : Matrix3x3) (h : A.charpoly = givenCharPoly) :
  ∃ P : Matrix3x3, P⁻¹ * A * P = F_A := by

why the lean don't know (F_A).charpoly is R[X],,i think it's obvious. :slight_smile:

[Robin Arnez]

This is probably some confusion with how variable works. variables only apply to every command individually, they don't create some kind of "scope", so what you wrote is equivalent to:

import Mathlib

open Matrix Polynomial

noncomputable section

def givenCharPoly {R : Type*} [Field R] : Polynomial R := (X - 2)^2 * (X + 1)

abbrev Matrix3x3 {R : Type*} [Field R] := Matrix (Fin 3) (Fin 3) R

instance {R : Type*} [Field R] : CommRing R := by
exact Field.toCommRing

def F_A {R : Type*} [Field R] : Matrix3x3 :=
  !![
    (0:R), (0:R), (-2:R);
    (1:R), (0:R), (-5:R);
    (0:R), (1:R), (-4:R)]

lemma F_A_charPoly : (F_A).charpoly = givenCharPoly := by
  sorry

variable {R : Type*} [Field R] in
example (A : Matrix3x3) (h : A.charpoly = givenCharPoly) :
  ∃ P : Matrix3x3, P⁻¹ * A * P = F_A := by

In particular, each R is an unrelated variable and they are not connected in any sense. Thus, Lean has no clue which R you mean when you write Matrix3x3. What you need to do is make R explicit when necessary:

variable {R : Type*} [Field R]

def givenCharPoly : Polynomial R := (X - 2)^2 * (X + 1)

abbrev Matrix3x3 (R : Type*) [Field R] := Matrix (Fin 3) (Fin 3) R

def F_A : Matrix3x3 R :=
  !![
    (0:R), (0:R), (-2:R);
    (1:R), (0:R), (-5:R);
    (0:R), (1:R), (-4:R)]

#check (F_A : Matrix3x3 R).charpoly

lemma F_A_charPoly : (F_A : Matrix3x3 R).charpoly = givenCharPoly := by
  sorry

example (A : Matrix3x3 R) (h : A.charpoly = givenCharPoly) :
    ∃ P : Matrix3x3 R, P⁻¹ * A * P = F_A := by
  sorry

[Hbz]

Thank you! :slight_smile:

[Hbz]

If i understand what you mean,i think the code you write

abbrev Matrix3x3 (R : Type*) [Field R] := Matrix (Fin 3) (Fin 3) R

should be

abbrev Matrix3x3 := Matrix (Fin 3) (Fin 3) R

right?

[Robin Arnez]

The opposite? In the second one Matrix3x3 takes R as an implicit parameter, so Lean has to determine its value from context. This is basically impossible though since Matrix3x3 is a Type _ regardless of what R you use, so you'd always have to write Matrix3x3 (R := R) in order for Lean to know what you mean. With (R : Type*), R becomes explicit so you specify it yourself (since Lean can't on its own)