Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-17 08:52 3053a169

View on Github →

feat(tactic/field_simp): tactic to reduce to one division in fields (#1792)

  • feat(algebra/field): simp set to reduce to one division in fields
  • tactic field_simp
  • fix docstring
  • fix build

Estimated changes

modified theorem two_ne_zero'
added theorem add_div'
added theorem div_add'
added theorem div_eq_iff
added theorem eq_div_iff
added theorem mul_div_assoc'
added theorem neg_div'
modified theorem inv_pow'
added theorem pow_div
modified theorem pow_ne_zero