Theorem Associates.prod_coe

Modification history

2023-03-21 09:26

Mathlib/RingTheory/UniqueFactorizationDomain.lean

feat: port RingTheory.UniqueFactorizationDomain (#3003)

Added Associates.prod_coe View on Github →