Commit 2022-12-27 05:52 814455ae

View on Github →

feat: port Algebra.Ring.Prod (#1229)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Ring/Prod.lean

added theorem NonUnitalRingHom.coe_fst

added theorem NonUnitalRingHom.coe_prodMap

added theorem NonUnitalRingHom.coe_snd

added def NonUnitalRingHom.fst

added theorem NonUnitalRingHom.fst_comp_prod

added def NonUnitalRingHom.prodMap

added theorem NonUnitalRingHom.prodMap_def

added theorem NonUnitalRingHom.prod_apply

added theorem NonUnitalRingHom.prod_comp_prodMap

added theorem NonUnitalRingHom.prod_unique

added def NonUnitalRingHom.snd

added theorem NonUnitalRingHom.snd_comp_prod

added theorem RingEquiv.coe_prod_comm

added theorem RingEquiv.coe_prod_comm_symm

added theorem RingEquiv.fst_comp_coe_prod_comm

added def RingEquiv.prodComm

added def RingEquiv.prodZeroRing

added theorem RingEquiv.snd_comp_coe_prod_comm

added def RingEquiv.zeroRingProd

added theorem RingHom.coe_fst

added theorem RingHom.coe_prodMap

added theorem RingHom.coe_snd

added def RingHom.fst

added theorem RingHom.fst_comp_prod

added def RingHom.prodMap

added theorem RingHom.prodMap_def

added theorem RingHom.prod_apply

added theorem RingHom.prod_comp_prodMap

added theorem RingHom.prod_unique

added def RingHom.snd

added theorem RingHom.snd_comp_prod

added theorem false_of_nontrivial_of_product_domain