Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-31 15:42 ff027743

View on Github →

feat(algebra/squarefree): norm_num extension for squarefree (#11666) Adds two methods for computing squarefree: an improved algorithm for VM computation of squarefreedom via the min_sq_fac function, and a proof procedure which follows the same evaluation strategy as a norm_num extension.

Estimated changes

Modified src/algebra/squarefree.lean

added def nat.min_sq_fac

added def nat.min_sq_fac_aux

added theorem nat.min_sq_fac_aux_has_prop

added theorem nat.min_sq_fac_dvd

added theorem nat.min_sq_fac_has_prop

added theorem nat.min_sq_fac_le_of_dvd

added theorem nat.min_sq_fac_prime

added def nat.min_sq_fac_prop

added theorem nat.min_sq_fac_prop_div

added theorem nat.squarefree_iff_min_sq_fac

added theorem nat.squarefree_iff_prime_squarefree

added theorem nat.squarefree_two

added theorem tactic.norm_num.not_squarefree_mul

added theorem tactic.norm_num.squarefree_bit10

added theorem tactic.norm_num.squarefree_bit1

added def tactic.norm_num.squarefree_helper

added theorem tactic.norm_num.squarefree_helper_0

added theorem tactic.norm_num.squarefree_helper_1

added theorem tactic.norm_num.squarefree_helper_2

added theorem tactic.norm_num.squarefree_helper_3

added theorem tactic.norm_num.squarefree_helper_4

Modified src/data/nat/prime.lean

modified theorem nat.min_fac_aux_has_prop

added theorem nat.min_fac_lemma

Modified test/norm_num_ext.lean