Theorem: IMOSL.IMO2010A1.Int_good_iff_MonoidGood (IMOSLLean4/IMO2010/A1/A1.lean)

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
f : ℤ → R
m n : ℤ
⊢ f (⌊m⌋ • n) = f m * ↑⌊f n⌋ ↔ f (m * n) = f m * ↑⌊f n⌋
Tactic:
rw [Int.floor_int, smul_eq_mul, id_def]
State after:
no goals