Zulip Chat Archive

Stream: general

Topic: with_infinitesimal


view this post on Zulip Kenny Lau (Feb 26 2019 at 09:29):

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

view this post on Zulip Kenny Lau (Feb 26 2019 at 09:29):

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

view this post on Zulip Kenny Lau (Feb 26 2019 at 09:29):

otherwise just ignore this thread


Last updated: May 15 2021 at 02:11 UTC