Theorem Nat.prod_factors_toFinset_of_squarefree

Modification history

2023-12-26 22:33

Mathlib/Data/Nat/Squarefree.lean

chore: Remove superfluous lemma that uses `n.factors.toFinset` (#9248) …

Deleted Nat.prod_factors_toFinset_of_squarefree 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 Nat.prod_factors_toFinset_of_squarefree View on Github →