Theorem: IncidenceAlgebra.mu_eq_mu' (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✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
⊢ mu 𝕜 = IncidenceAlgebra.mu' 𝕜
Tactic:
classical
exact left_inv_eq_right_inv (mu_mul_zeta _ _) (zeta_mul_mu' _ _)
State after:
no goals

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✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
⊢ mu 𝕜 = IncidenceAlgebra.mu' 𝕜
Tactic:
exact left_inv_eq_right_inv (mu_mul_zeta _ _) (zeta_mul_mu' _ _)
State after:
no goals