Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-10 03:23 56c4919a

View on Github →

feat(tactic/abel): decision procedure for comm groups

Estimated changes

Modified algebra/group_power.lean

added theorem gsmul_add

added theorem gsmul_zero

added theorem mul_gpow

modified theorem one_gpow

Created tactic/abel.lean

added theorem tactic.abel.const_add_term

added theorem tactic.abel.const_add_termg

added inductive tactic.abel.normalize_mode

added def tactic.abel.smul

added def tactic.abel.smulg

added theorem tactic.abel.subst_into_smul

added theorem tactic.abel.subst_into_smulg

added def tactic.abel.term

added theorem tactic.abel.term_add_const

added theorem tactic.abel.term_add_constg

added theorem tactic.abel.term_add_term

added theorem tactic.abel.term_add_termg

added theorem tactic.abel.term_atom

added theorem tactic.abel.term_atomg

added theorem tactic.abel.term_neg

added theorem tactic.abel.term_smul

added theorem tactic.abel.term_smulg

added def tactic.abel.termg

added theorem tactic.abel.unfold_gsmul

added theorem tactic.abel.unfold_smul

added theorem tactic.abel.unfold_smulg

added theorem tactic.abel.unfold_sub

added theorem tactic.abel.zero_smul

added theorem tactic.abel.zero_smulg

added theorem tactic.abel.zero_term

added theorem tactic.abel.zero_termg

Modified tactic/norm_num.lean

added theorem norm_num.subst_into_neg

Modified tactic/ring.lean

deleted def horner

modified theorem tactic.ring.add_neg_eq_sub

added def tactic.ring.horner

deleted theorem tactic.ring.subst_into_neg

Modified tactic/ring2.lean