Skip to content

chore(Data/Int/WithZero): use log in WithZeroMulInt.toNNReal - #43589

Open
mariainesdff wants to merge 1 commit into
leanprover-community:masterfrom
mariainesdff:tonnreal_log
Open

chore(Data/Int/WithZero): use log in WithZeroMulInt.toNNReal#43589
mariainesdff wants to merge 1 commit into
leanprover-community:masterfrom
mariainesdff:tonnreal_log