exact left_inv_eq_right_inv (mu_mul_zeta _ _) (zeta_mul_mu' _ _)
𝕄 : 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' 𝕜
no goals