I found out that 9 * 0.0001 = 0.0009000000000000001, but 9 / 10_000 = 0.0009
Is it guaranteed that when you divide by power of 10 you will receive exact value (by IEEE 754-2019: IEEE Standard for Floating-Point Arithmetic)
I am expecting someone who knows specific behavior of Floating-point standard to explain if there is such guarantees or not.
0.009 cannot be represented precisely by IEEE 754 floating point. The binary representation of 0.009 would be:
0.0000001001001101110100101111000110101001111110111110011101101100100010110100001110010101100000010000011
0001001001101110100101111000110101001111110111110011101101100100010110100001110010101100000010000011
...
It is a rational number with an infinite number of (binary) digits after the decimal point.
So this cannot be represented in floating point which only has a finite number of binary digits available in the mantissa part.
0.009 in floating point is represented as follows:
sign exponent mantissa
0 01111000 00100110111010010111100
But as the binary sequence is finite here, it actually represents this number:
0.0089999996125698089599609375....
A similar deviation will occur for other positive powers of 10 in 9/10n
You can make the conversion using this tool.