Theorem: IMOSL.IMO2010A1.MonoidGood.map_eq_map_one_mul_floor (IMOSLLean4/IMO2010/A1/A1Monoid.lean)

State before:
R : Type u_1
M : Type u_2
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : MulOneClass M
f : M → R
hf : MonoidGood f
x : M
⊢ f x = f 1 * ↑⌊f x⌋
Tactic:
rw [← hf, one_mul]
State after:
no goals