Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-24 09:57 f7f12bc6

View on Github →

feat(data/nat/prime): norm_num plugin for factors (#8009) Implements a norm_num plugin to evaluate terms like nat.factors 231 = [3, 7, 11].

Estimated changes

Modified src/data/nat/prime.lean

added theorem nat.factors_chain'

added theorem nat.factors_chain

added theorem nat.factors_chain_2

added theorem nat.factors_sorted

added theorem nat.le_min_fac'

added theorem nat.le_min_fac

added def tactic.norm_num.factors_helper

added theorem tactic.norm_num.factors_helper_cons'

added theorem tactic.norm_num.factors_helper_cons

added theorem tactic.norm_num.factors_helper_end

added theorem tactic.norm_num.factors_helper_nil

added theorem tactic.norm_num.factors_helper_same

added theorem tactic.norm_num.factors_helper_same_sn

added theorem tactic.norm_num.factors_helper_sn

Modified src/tactic/norm_num.lean

Modified test/norm_num.lean