Commit 2024-09-18 18:31 38dfa07f

View on Github →

chore: avoid Finset dependency in Algebra.Algebra.Defs (#16893)

Estimated changes

Modified Mathlib/Algebra/Algebra/Basic.lean

added theorem algebraMap.coe_prod

added theorem algebraMap.coe_sum

Modified Mathlib/Algebra/Algebra/Defs.lean

deleted theorem algebraMap.coe_prod

deleted theorem algebraMap.coe_sum