mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(algebra/order/digits): the digits of a linear_ordered_semifield

Open eric-wieser opened this issue 2 years ago • 0 comments

This aims to generalize some of the nnreal_binary stuff in LTE.

https://github.com/leanprover-community/lean-liquid/blob/b9b42a840d2416657d7ba173f5d20e24906e6137/src/for_mathlib/nnreal_int_binary.lean#L136-L140

Open in Gitpod

eric-wieser avatar May 25 '22 12:05 eric-wieser