Commit 2019-08-04 04:21 b46665fa

chore(ring_theory/algebra): make first type argument explicit in alg_hom (#1296)

• chore(ring_theory/algebra): make first type argument explicit in alg_hom Now this works, and it didn't work previously even with @

structure alg_equiv (α β γ : Type*) [comm_ring α] [ring β] [ring γ]
  [algebra α β] [algebra α γ] extends alg_hom α β γ :=

• Update algebra.lean