Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-10 12:50 363a286b

View on Github →

chore(*): speedup slow proofs (#7148) Some proofs using heavy rfl or heavy obviously can be sped up considerably. Done in this PR for some outstanding examples.

Estimated changes

Modified src/algebra/category/Algebra/basic.lean

Modified src/algebra/category/Algebra/limits.lean

Modified src/algebra/category/CommRing/limits.lean

added def CommRing.is_limit_lifted_cone

added def CommRing.lifted_cone

added def CommSemiRing.is_limit_lifted_cone

added def CommSemiRing.lifted_cone

Modified src/algebra/category/Group/colimits.lean

Modified src/analysis/normed_space/hahn_banach.lean

Modified src/category_theory/monoidal/internal/Module.lean

Modified src/data/mv_polynomial/equiv.lean

Modified src/linear_algebra/char_poly/coeff.lean

Modified src/linear_algebra/eigenspace.lean

Modified src/linear_algebra/exterior_algebra.lean

Modified src/ring_theory/finiteness.lean

Modified src/ring_theory/polynomial/basic.lean

Modified src/ring_theory/witt_vector/structure_polynomial.lean