Strict ordered semiring have characteristic zero

@[instance 100]

instance StrictOrderedSemiring.to_charZero {α : Type u_1} [StrictOrderedSemiring α] : CharZero α

Equations

• ⋯ = ⋯