Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-18 21:14 e719f8ee

View on Github →

chore(*): switch to lean 3.7.1c (#2106)

  • fix(deprecated/group): remove dangerous instances
  • Update Lean version to nightly.
  • Remove composition instances for group homomorphisms.
  • Remove dangerous is_submonoid instances.
  • Flip instance arguments.
  • Various Lean 3.7 fixes.
  • Correctly use lemma.
  • Use new elan 0.8.0 lean version name.
  • Remove dangerous *.comp instances.
  • Fix comp instance fallout.
  • Fix more *.comp fallout
  • Fix more *.comp fallout.
  • More *.comp fallout.
  • Fix *.comp fallout
  • Fix *.comp fallout
  • Port to has_attribute and copy_attribute changes.
  • Fix monad_writer_adapter_trans instance.
  • Revert 3.6 hacks.
  • Update library note for *.comp morphisms.
  • fix(scripts/deploy_docs.sh): use lean_version from mathlib leanpkg.toml
  • Do not mention is_mul_hom.mul in library note.
  • Update lean version to 3.7.0.
  • Remove of_tactic'
  • switch to 3.7.1c

Estimated changes

modified theorem direct_sum.to_group.unique
added theorem is_ring_hom.comp
added theorem is_semiring_hom.comp
added theorem is_group_hom.comp
added theorem is_monoid_hom.comp
added theorem is_mul_hom.comp