natDegree_det_X_add_C_le — Mathlib

English

For matrices A,B over a commutative ring, the natural degree of the determinant of X·A.map C + B.map C is at most the cardinality of n.

Русский

Для матриц A,B над коммутативным кольцом естественная степень детерминанта детерминанта от $X·A\mapsto C + B\mapsto C$ не превосходит кардинал множества n.

LaTeX

$$$\\operatorname{natDegree}\\big(\\det\\big((X : \\alpha[X]) \\cdot A.map C + B.map C\\big)\\big) \\le |n|$$$

Lean4

theorem natDegree_det_X_add_C_le (A B : Matrix n n α) :
    natDegree (det ((X : α[X]) • A.map C + B.map C : Matrix n n α[X])) ≤ Fintype.card n :=
  by
  rw [det_apply]
  refine (natDegree_sum_le _ _).trans ?_
  refine Multiset.max_le_of_forall_le _ _ ?_
  simp only [forall_apply_eq_imp_iff, true_and, Function.comp_apply, Multiset.mem_map, exists_imp, Finset.mem_univ_val]
  intro g
  calc
    natDegree (sign g • ∏ i : n, (X • A.map C + B.map C : Matrix n n α[X]) (g i) i) ≤
        natDegree (∏ i : n, (X • A.map C + B.map C : Matrix n n α[X]) (g i) i) :=
      by
      rcases Int.units_eq_one_or (sign g) with sg | sg
      · rw [sg, one_smul]
      · rw [sg, Units.neg_smul, one_smul, natDegree_neg]
    _ ≤ ∑ i : n, natDegree (((X : α[X]) • A.map C + B.map C : Matrix n n α[X]) (g i) i) :=
      (natDegree_prod_le (Finset.univ : Finset n) fun i : n => (X • A.map C + B.map C : Matrix n n α[X]) (g i) i)
    _ ≤ Finset.univ.card • 1 := (Finset.sum_le_card_nsmul _ _ 1 fun (i : n) _ => ?_)
    _ ≤ Fintype.card n := by simp [mul_one, Finset.card_univ]
  dsimp only [add_apply, smul_apply, map_apply, smul_eq_mul]
  compute_degree

Похожие утверждения