Commit 2023-05-25 17:58 a1c58a9b

View on Github →

feat: port Data.Nat.Squarefree (#4278)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Squarefree.lean

added def Nat.MinSqFacProp

added theorem Nat.Squarefree.ext_iff

added theorem Nat.Squarefree.factorization_le_one

added theorem Nat.divisors_filter_squarefree

added def Nat.minSqFac

added def Nat.minSqFacAux

added theorem Nat.minSqFacAux_has_prop

added theorem Nat.minSqFacProp_div

added theorem Nat.minSqFac_dvd

added theorem Nat.minSqFac_has_prop

added theorem Nat.minSqFac_le_of_dvd

added theorem Nat.minSqFac_prime

added theorem Nat.sq_mul_squarefree

added theorem Nat.sq_mul_squarefree_of_pos'

added theorem Nat.sq_mul_squarefree_of_pos

added theorem Nat.squarefree_and_prime_pow_iff_prime

added theorem Nat.squarefree_iff_factorization_le_one

added theorem Nat.squarefree_iff_minSqFac

added theorem Nat.squarefree_iff_nodup_factors

added theorem Nat.squarefree_iff_prime_squarefree

added theorem Nat.squarefree_mul

added theorem Nat.squarefree_of_factorization_le_one

added theorem Nat.squarefree_pow_iff

added theorem Nat.squarefree_two

added theorem Nat.sum_divisors_filter_squarefree

added def SquarefreeHelper

added theorem not_squarefree_mul

added theorem squarefreeHelper_1

added theorem squarefreeHelper_2

added theorem squarefreeHelper_3

added theorem squarefreeHelper_4

added theorem squarefree_bit10

added theorem squarefree_bit1

added theorem squarefree_helper_0