Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-07 03:43 c718a229

View on Github →

feat(extensionality): rename to ext; generate ext rules for structures (#1645)

  • Update core.lean
  • Update tactics.lean
  • integrate generation of extensionality lemma of structures into ext
  • Update src/tactic/ext.lean [skip ci] Co-Authored-By: Rob Lewis Rob.y.lewis@gmail.com
  • Update src/tactic/ext.lean [skip ci] Co-Authored-By: Rob Lewis Rob.y.lewis@gmail.com
  • Update src/tactic/ext.lean Co-Authored-By: Rob Lewis Rob.y.lewis@gmail.com
  • Update ext.lean [skip ci]
  • Update tactics.md [skip ci]
  • fix build
  • fix build

Estimated changes

modified theorem units.ext
modified theorem linear_map.ext
modified theorem submodule.ext
modified theorem ring_hom.ext
modified theorem category_theory.iso.ext
modified theorem ring_equiv.ext
modified theorem equiv.ext
modified theorem equiv.perm.ext
modified theorem finmap.ext
modified theorem alist.ext
modified theorem matrix.ext
modified theorem option.ext
modified theorem pequiv.ext
modified theorem polynomial.ext
modified theorem setoid.ext'
modified theorem vector.ext
modified theorem linear_equiv.ext
modified theorem bilin_form.ext
modified theorem direct_sum.ext
modified theorem sesq_form.ext
modified theorem function.embedding.ext
modified theorem measurable_space.ext
modified theorem measure_theory.measure.ext
modified theorem subalgebra.ext
modified theorem ideal.ext
modified theorem mv_power_series.ext
modified theorem power_series.ext
modified theorem plift.ext
modified theorem ulift.ext
modified theorem continuous_linear_map.ext
modified theorem topological_space.opens.ext
modified theorem df.ext
modified theorem unit.ext
added structure foo