Theorem: IncidenceAlgebra.mu'Aux_apply (LeanCamCombi/Incidence.lean)

State before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ IncidenceAlgebra.mu'Aux 𝕜 b a = if a = b then 1 else -∑ x ∈ (Ioc a b).attach, IncidenceAlgebra.mu'Aux 𝕜 b ↑x
Tactic:
rw [mu'Aux]
State after:
no goals