Strict ordered semiring have characteristic zero

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

Equations

• ⋯ = ⋯