Theorem Squarefree.nodup_factors

Modification history

2024-07-17 17:39

Mathlib/Data/Nat/Squarefree.lean

chore: Rename `Nat.factors` to `Nat.primeFactorsList` (#13832) …

Deleted Squarefree.nodup_factors View on Github →

2023-08-18 07:22

Mathlib/Data/Nat/Squarefree.lean

feat(Data/Nat/Squarefree): Add lemmas about the product of distinct factors of a squarefree `Nat` (#6344) …

Added Squarefree.nodup_factors View on Github →