Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-26 23:31 f0bb2f82

View on Github →

feat(ring_theory/polynomial): mv_polynomial.integral_domain (#2021)

  • feat(ring_theory/polynomial): mv_polynomial.integral_domain
  • Add docstrings
  • Add docstrings
  • Fix import
  • Fix build
  • Please linter, please
  • Update src/algebra/ring.lean
  • Clean up code, process comments
  • Update src/data/equiv/fin.lean
  • Update src/data/equiv/fin.lean
  • Update src/data/equiv/fin.lean
  • Update src/ring_theory/polynomial.lean

Estimated changes

added structure is_integral_domain
added def fin_succ_equiv
added def fin_zero_equiv'