Theorem: IMOSL.IMO2012A5.PeriodEquiv.mul_right_equiv (IMOSLLean4/IMO2012/A5/A5General/A5Periodic.lean)

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c d : R
h : (PeriodEquiv f) c d
a : R
⊢ (PeriodEquiv f) (c * a) (d * a)
Tactic:
rw [iff_sub, ← sub_mul]
State after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c d : R
h : (PeriodEquiv f) c d
a : R
⊢ (PeriodEquiv f) ((c - d) * a) 0

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c d : R
h : (PeriodEquiv f) c d
a : R
⊢ (PeriodEquiv f) ((c - d) * a) 0
Tactic:
exact mul_right_equiv_zero hf (iff_sub.mp h) a
State after:
no goals