(Probably) regarding type conversion

Stream: new members

[Hbz]

import Mathlib

open Polynomial

noncomputable section

variables {F : Type*} [Field F] (f g h : F[X])

/-! ### Definition: Reciprocal Polynomial -/

/-- The reciprocal of a polynomial `f` with degree `n` is defined as `x^n * f(1/x)`.

    This requires that `f ≠ 0` and `f(0) ≠ 0` to be well-defined. -/

@[simp]noncomputable def reciprocal (f : Polynomial F) : Polynomial F :=

  Polynomial.reverse f

notation f "⁎" => reciprocal f

/-! ### Lemma: Double reciprocal -/

@[simp]

lemma natDegree_reverse {R : Type*} [Semiring R] {f : R[X]} (he : f.coeff 0 ≠ 0) :

    f.reverse.natDegree = f.natDegree := by

  simp [*, natDegree_eq_reverse_natDegree_add_natTrailingDegree f, natTrailingDegree_eq_zero_of_constantCoeff_ne_zero]

/-! ### Lemma: Double reciprocal -/

lemma reciprocal_involutive (hf : f ≠ 0 ∧ f.eval 0 ≠ 0) : (f⁎)⁎ = f := by

  have hc0 : f.coeff 0 ≠ 0 := by

    cases hf

    rwa [ne_eq, coeff_zero_eq_eval_zero]

  ext n

  simp only [reciprocal, coeff_reverse, revAt]

  have (hn : n ≤ f.natDegree) : f.natDegree - (f.natDegree - n) = n := Nat.sub_sub_self hn

  aesop

/-! ## Theorem 3.12: Irreducibility of reciprocal -/

/-- If `f` is irreducible and `f(0) ≠ 0`, then `f⁎` is also irreducible. -/

theorem reciprocal_irreducible (hf : Irreducible f) (h0 : f.eval 0 ≠ 0) : Irreducible (f⁎) :=

  sorry

/-! ## Theorem 3.13: Structure of self-reciprocal polynomials -/

/-- A polynomial is self-reciprocal if it equals its reciprocal. -/

def self_reciprocal (f : F[X]) : Prop := f ≠ 0 ∧ f⁎ = f

#check associated_of_dvd_dvd

#check Associated

/-- The structure of a self-reciprocal polynomial with two irreducible factors. -/

theorem self_reciprocal_factor_structure

  (hf : f = g * h)

  (hg : Irreducible g) (hh : Irreducible h)

  (h0g : g.eval 0 ≠ 0) (h0h : h.eval 0 ≠ 0)

  (hs : self_reciprocal f) :

  (∃ a : Fˣ, h⁎ = a • g) ∨ (∃ b : Fˣ, b ^ 2 = 1 ∧ g⁎ = b • g ∧ h⁎ = b • h) := by

  rw[self_reciprocal] at hs

  rcases hs with ⟨h1,h2⟩

  rw[hf] at h2

  have h3 :(g * h)⁎ = g⁎ * h⁎ := by simp

  rw[h3] at h2
--shit ()

  have h4 : Irreducible (g⁎) := by

    exact reciprocal_irreducible g hg h0g

  have h5 : Irreducible (h⁎) := by

    exact reciprocal_irreducible h hh h0h

  have prime_g : Prime g := irreducible_iff_prime.mp hg

  have g_dvd : g ∣ g⁎ * h⁎ := by exact Dvd.intro h (id (Eq.symm h2))

  rcases prime_g.dvd_mul.mp g_dvd with (dvd_g' | dvd_h')
--在写代码的时候发现have命名对于定理证明有很大帮助

  ·

    have : Associated g (g⁎) := Irreducible.associated_of_dvd hg h4 dvd_g'

    obtain ⟨u, hu⟩ := this

    have u_unit : IsUnit (u : F[X]) := Units.isUnit u

    rcases (Polynomial.isUnit_iff).1 u_unit with ⟨c, c_unit⟩

    have c_ne_zero : c ≠ 0 := by

      sorry

    sorry

  ·

    have : Associated g (h⁎) := Irreducible.associated_of_dvd hg h5 dvd_h'

    obtain ⟨u, hu⟩ := this

    -- 将多项式单位 u 转换为域单位

    have u_unit : IsUnit (u : F[X]) := Units.isUnit u

    rcases (Polynomial.isUnit_iff).1 u_unit with ⟨a, a_unit⟩

    -- 确保 a ≠ 0

    sorry

I don't know how to convert g * ↑u = h⁎ into h⁎ = a • g, even though this seems very simple.

[Hbz]

I think i have some ideas. :rolling_on_the_floor_laughing: