Zulip Chat Archive
Stream: new members
Topic: help to prove roots = {a,b} (a = b)
Alex (Apr 05 2025 at 07:56):
How to prove when A 0 0 = A 1 1? Thank you very much!
import Mathlib
variable {n : Type*} [DecidableEq n] [Fintype n]
variable {R : Type v} {M : Type w} [Field R]
variable [AddCommGroup M] [Module R M]
open Matrix Polynomial Module
noncomputable def det_charmatrix2x2_charpoly (A : Matrix (Fin 2) (Fin 2) R): R[X] := X^2 -(C (A 0 0) + C (A 1 1)) * X + C (A 0 0) * C (A 1 1) - C (A 0 1) * C (A 1 0)
lemma det_charmatrix2x2_charpoly_apply (A : Matrix (Fin 2) (Fin 2) R) : A.charmatrix.det = det_charmatrix2x2_charpoly A :=by
unfold charmatrix
unfold det_charmatrix2x2_charpoly
simp [Matrix.det_fin_two]
rw [sub_mul,mul_sub,← pow_two,mul_sub,sub_sub,sub_add]
congr 1
rw [add_sub,mul_comm,← add_mul,add_comm]
lemma roots_char_trimatrix2x2 (A : Matrix (Fin 2) (Fin 2) R) (hA : A 0 1 = 0 ∨ A 1 0 = 0) (hA' : A 0 0 ≠ 0 ∧ A 1 1 ≠ 0):(det_charmatrix2x2_charpoly A).roots = {A 0 0, A 1 1} := by
have isroot :(det_charmatrix2x2_charpoly A).IsRoot (A 0 0) ∧ (det_charmatrix2x2_charpoly A).IsRoot (A 1 1) := by{
rw [det_charmatrix2x2_charpoly]
rcases hA with (h1 | h2)
-- A 0 1 = 0
· {
simp [h1,zero_mul]
split_ands
repeat simp [add_mul,sub_add,← add_sub,mul_comm (A 1 1) (A 0 0),pow_two]
}
· {
simp [h2,mul_zero]
split_ands
repeat simp [add_mul,sub_add,← add_sub,mul_comm (A 1 1) (A 0 0),pow_two]
}
}
symm
have hp0 : det_charmatrix2x2_charpoly A ≠ 0 := by
rw [det_charmatrix2x2_charpoly]
apply_fun (·.coeff 2)
simp
by_cases h : (A 0 0) ≠ (A 1 1)
· {
refine Multiset.eq_of_le_of_card_le ?_ ?_
· rw [Multiset.le_iff_subset (by simp [h])]
intro a ha
simp? at ha says simp only [Multiset.insert_eq_cons, Multiset.mem_cons, Multiset.mem_singleton] at ha
obtain rfl | rfl := ha
· simpa [hp0] using isroot.1
· simpa [hp0] using isroot.2
· rw [Multiset.insert_eq_cons, Multiset.card_cons, Multiset.card_singleton]
suffices h : (det_charmatrix2x2_charpoly A).natDegree = 1 + 1 from h ▸ (det_charmatrix2x2_charpoly A).card_roots'
rw [det_charmatrix2x2_charpoly]
compute_degree!
}
· {
simp at h
simp [h]
sorry -- A 1 1 ::ₘ {A 1 1} = (det_charmatrix2x2_charpoly A).roots
}
Last updated: May 02 2025 at 03:31 UTC