with_infinitesimal

Stream: general

[Kenny Lau]

import data.polynomial

universes u v

def with_infinitesimal (α : Type u) [comm_semiring α] : Type u := polynomial α

instance {α : Type u} [comm_semiring α] [decidable_eq α] :
  comm_semiring (with_infinitesimal α) :=
polynomial.comm_semiring

instance {α : Type u} [comm_ring α] [decidable_eq α] :
  comm_ring (with_infinitesimal α) :=
polynomial.comm_ring


namespace polynomial

variables {α : Type u} [comm_semiring α] [decidable_eq α]

def undegree (p : polynomial α) : with_top ℕ :=
finset.inf p.support coe

def nat_undegree (p : polynomial α) : ℕ :=
option.get_or_else (undegree p) 0

def trailing_coeff (p : polynomial α) : α :=
p.coeff p.nat_undegree

end polynomial


namespace with_infinitesimal

variables {α : Type u} [comm_semiring α] [decidable_eq α]

def ε : with_infinitesimal α := polynomial.X

def C : α → with_infinitesimal α := polynomial.C

end with_infinitesimal


namespace with_infinitesimal

variables {α : Type u} [linear_ordered_comm_ring α] [decidable_eq α]

def nonneg (p : with_infinitesimal α) : Prop :=
0 ≤ p.trailing_coeff

instance : linear_ordered_comm_ring (with_infinitesimal α) :=
{ le := λ p q, nonneg (q - p),
  .. with_infinitesimal.comm_ring }

end with_infinitesimal

[Kenny Lau]

so I started this, and didn't want to continue; someone might want to continue

[Kenny Lau]

otherwise just ignore this thread