Strict ordered semiring have characteristic zero

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

Equations

• @StrictOrderedSemiring.to_charZero = @StrictOrderedSemiring.to_charZero.proof_1