Def Associates.FactorSetMem

Modification history

2024-11-20 11:43

Mathlib/RingTheory/UniqueFactorizationDomain.lean

chore(RingTheory): split `UniqueFactorizationDomain.lean` (#19256) …

Modified Associates.FactorSetMem View on Github →

2024-09-03 05:37

Mathlib/RingTheory/UniqueFactorizationDomain.lean

chore: merge bump/v4.12.0 and move toolchain to v4.12.0-rc1 (#16433)

Modified Associates.FactorSetMem View on Github →

2023-03-21 09:26

Mathlib/RingTheory/UniqueFactorizationDomain.lean

feat: port RingTheory.UniqueFactorizationDomain (#3003)

Added Associates.FactorSetMem View on Github →