Commit 2023-05-17 06:40 4e3c1517

View on Github →

feat: port Algebra.DirectSum.Ring (#1968)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/DirectSum/Ring.lean

added def DirectSum.gMulHom

added def DirectSum.liftRingHom

added theorem DirectSum.list_prod_ofFn_of_eq_dProd

added def DirectSum.mulHom

added theorem DirectSum.mulHom_apply

added theorem DirectSum.mulHom_of_of

added theorem DirectSum.mul_eq_dfinsupp_sum

added theorem DirectSum.mul_eq_sum_support_ghas_mul

added theorem DirectSum.ofIntCast

added theorem DirectSum.ofList_dProd

added theorem DirectSum.ofNatCast

added theorem DirectSum.ofPow

added def DirectSum.ofZeroRingHom

added theorem DirectSum.of_eq_of_gradedMonoid_eq

added theorem DirectSum.of_mul_of

added theorem DirectSum.of_zero_mul

added theorem DirectSum.of_zero_one

added theorem DirectSum.of_zero_pow

added theorem DirectSum.of_zero_smul

added theorem DirectSum.ringHom_ext'

added theorem DirectSum.ringHom_ext

added def DirectSum.toSemiring

added theorem DirectSum.toSemiring_coe_addMonoidHom

added theorem DirectSum.toSemiring_of