Def RingEquiv.zeroRingProd

Modification history

2022-12-29 15:12
Mathlib/Algebra/Ring/Prod.lean
chore: tidy various files (#1247)
Modified RingEquiv.zeroRingProdView on Github →
2022-12-27 05:52
Mathlib/Algebra/Ring/Prod.lean
feat: port Algebra.Ring.Prod (#1229)
Added RingEquiv.zeroRingProdView on Github →