Commit 2023-06-17 08:04 6ffd1a5d

View on Github →

chore: cleanup of some ext porting notes (#5176)

Estimated changes

Modified Mathlib/Algebra/ContinuedFractions/Basic.lean

Modified Mathlib/Algebra/DirectSum/Basic.lean

Modified Mathlib/Algebra/DirectSum/Ring.lean

Modified Mathlib/Algebra/Free.lean

Modified Mathlib/Algebra/FreeMonoid/Basic.lean

modified theorem FreeMonoid.comp_lift

Modified Mathlib/Data/Bitvec/Lemmas.lean

Modified Mathlib/Data/Dfinsupp/Multiset.lean

Modified Mathlib/Data/Finsupp/Basic.lean