Theorem Associates.count_mul_of_coprime'

Modification history

2024-11-20 11:43

Mathlib/RingTheory/UniqueFactorizationDomain.lean

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

Modified Associates.count_mul_of_coprime'View on Github →

2024-08-07 05:28

Mathlib/RingTheory/UniqueFactorizationDomain.lean

chore: backports for leanprover/lean4#4814 (part 17) (#15429) …

Modified Associates.count_mul_of_coprime'View on Github →

2024-03-15 12:53

Mathlib/RingTheory/UniqueFactorizationDomain.lean

fix: remove DecidableEq assumption from `factors` (#11158) …

Modified Associates.count_mul_of_coprime'View on Github →

2023-03-21 09:26

Mathlib/RingTheory/UniqueFactorizationDomain.lean

feat: port RingTheory.UniqueFactorizationDomain (#3003)

Added Associates.count_mul_of_coprime'View on Github →