Theorem: ArithmeticFunction.IsMultiplicative.mult_lcm_eq_of_ne_zero (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean)

State before:
R : Type u_1
inst✝ : CommGroupWithZero R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
x y : ℕ
hf : f (x.gcd y) ≠ 0
⊢ f (x.lcm y) = f x * f y / f (x.gcd y)
Tactic:
rw [←h_mult.lcm_apply_mul_gcd_apply]
State after:
R : Type u_1
inst✝ : CommGroupWithZero R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
x y : ℕ
hf : f (x.gcd y) ≠ 0
⊢ f (x.lcm y) = f (x.lcm y) * f (x.gcd y) / f (x.gcd y)

State before:
R : Type u_1
inst✝ : CommGroupWithZero R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
x y : ℕ
hf : f (x.gcd y) ≠ 0
⊢ f (x.lcm y) = f (x.lcm y) * f (x.gcd y) / f (x.gcd y)
Tactic:
field_simp
State after:
no goals