We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 480f2d6 commit 2f5cc10Copy full SHA for 2f5cc10
Mathlib/Algebra/Free.lean
@@ -521,7 +521,7 @@ a semigroup `β`. -/
521
homomorphism `FreeAddSemigroup α → β` given an additive semigroup `β`. -/]
522
def lift : (α → β) ≃ (FreeSemigroup α →ₙ* β) where
523
toFun f :=
524
- { toFun := fun x ↦ x.2.foldl (fun a b ↦ a * f b) (f x.1)
+ { toFun x := x.2.foldl (fun a b ↦ a * f b) (f x.1)
525
map_mul' := by simp [← List.foldl_map, List.foldl_assoc] }
526
invFun f := f ∘ of
527
0 commit comments