Commit 2021-08-16 20:42 e1048963

View on Github →

ring tactic (#33)

  • aligned tactic names to mathport
  • added byContra tactic
  • added guardExprEq guardTarget guardHyp
  • added introv
  • Update Mathlib/Tactic/Basic.lean
  • Update Mathlib/Tactic/Basic.lean
  • added exacts
  • use of elab and examples
  • matchTarget
  • byContra all cases
  • sorry & iterate
  • fix : get to build
  • fix : get to build
  • fix : get to build 3
  • fix : alpha eq in guardHyp but consuming mdata
  • feat : repeat' tactic
  • feat : anyGoals tactic
  • feat(Algebra/Group/Defs): Monoid lemmas
  • feat(Tactic/Ring): starting ring
  • fix: fixed normNum
  • fix : compatibility Numeric.ofNat with One.one and Zero.zero
  • fix : removed print
  • fix: fixed normNum
  • feat: ring with only additions and one variable
  • feat: ring tactic furnctional for addition and multiplication
  • feat(Algebra) : more lemmas
  • feat (Tactic/NormNum) : normNum exponentiation
  • feat (Tactic/Ring) : exponentiation for ring
  • fix : updated with new version of mkNatLit
  • fix : import ring
  • chore : update to newer lean version
  • doc (Tactic/Ring) : add author
  • fix(Algebra/Group/Defs) : Monoid.npow
  • chore(Tactic/Ring) : updated to new lean version

Estimated changes

modified theorem mul_one
added theorem mul_pow
modified theorem npow_eq_pow
deleted theorem npow_succ'
deleted theorem npow_zero'
modified theorem one_mul
added theorem pow_add
added theorem pow_mul
added theorem pow_mul_comm
added theorem pow_one
added theorem pow_succ'
added theorem pow_succ
added theorem pow_zero
added theorem Nat.ofNat_eq_Nat
added theorem Semiring.ofNat_pow
added theorem add_mul
added theorem mul_add
added theorem mul_zero
added theorem zero_mul
added structure Tactic.Ring.Cache
added inductive Tactic.Ring.HornerExpr
added structure Tactic.Ring.State
added theorem Tactic.Ring.horner_pow
added def Tactic.Ring.run