Theorem: lxyab (RMT4/hurwitz.lean)

State before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y✝ : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
x y a b : 𝕜
⊢ x * a - y * b = (x - y) * a + y * (a - b)
Tactic:
ring
State after:
no goals