Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-27 05:41 2fc9b158

View on Github →

chore(data/real/*): use bundled homs to prove coe_sum etc (#2533)

Estimated changes

Modified src/algebra/big_operators.lean

added theorem ring_hom.map_list_prod

added theorem ring_hom.map_list_sum

added theorem ring_hom.map_multiset_prod

added theorem ring_hom.map_multiset_sum

Modified src/data/real/ennreal.lean

added theorem ennreal.coe_of_nnreal_hom

added def ennreal.of_nnreal_hom

Modified src/data/real/nnreal.lean

added theorem nnreal.coe_to_real_hom

added def nnreal.to_real_hom