Strict ordered semiring have characteristic zero

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

Equations

• (_ : CharZero α) = (_ : CharZero α)