how to prove (f⁎)⁎ = f

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 -/
lemma reciprocal_involutive (hf : f ≠ 0 ∧ f.eval 0 ≠ 0) : (f⁎)⁎ = f := by sorry
--f is just a polynomial

[Ruben Van de Velde]

Not sure, if you don't tell us what f is

[Hbz]

Ruben Van de Velde said:

Not sure, if you don't tell us what f is

f is an arbitrary polynomial.

[Kenny Lau]

Use Polynomial.coeff_reverse

[Damiano Testa]

I think that you made your life harder by using ∧, the "non-standard" f.eval 0, as well as introducing the reciprocal definition.

@[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

[Notification Bot]

This topic was moved here from #lean4 > how to prove (f⁎)⁎ = f by Damiano Testa.

[Hbz]

Kenny Lau said:

Use Polynomial.coeff_reverse

Thank you very much.

[Hbz]

Damiano Testa said:

I think that you made your life harder by using ∧, the "non-standard" f.eval 0, as well as introducing the reciprocal definition.

@[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

Oh my god!
Thank you! :+1: