Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-19 20:59 72cb2e82

View on Github →

refactor(*): rename some declarations ending with '' (#9504)

Estimated changes

Modified src/algebra/algebra/basic.lean

deleted theorem algebra.smul_def''

Modified src/algebra/algebra/tower.lean

Modified src/algebra/free.lean

deleted def free_magma.rec_on'

added def free_magma.rec_on_mul

deleted def free_semigroup.rec_on'

added def free_semigroup.rec_on_pure

Modified src/algebra/group_power/order.lean

deleted theorem pow_lt_pow''

added theorem pow_lt_pow'

Modified src/algebra/monoid_algebra/basic.lean

Modified src/algebra/support.lean

deleted theorem function.mul_support_inv''

added theorem function.mul_support_inv'

Modified src/category_theory/abelian/exact.lean

deleted theorem category_theory.abelian.exact_iff''

added theorem category_theory.abelian.exact_iff_image_eq_kernel

Modified src/category_theory/monoidal/natural_transformation.lean

deleted theorem category_theory.monoidal_nat_trans.comp_to_nat_trans''

deleted theorem category_theory.monoidal_nat_trans.comp_to_nat_trans'

added theorem category_theory.monoidal_nat_trans.comp_to_nat_trans

added theorem category_theory.monoidal_nat_trans.comp_to_nat_trans_lax

Modified src/data/matrix/basic.lean

Modified src/field_theory/abel_ruffini.lean

Modified src/field_theory/fixed.lean

Modified src/field_theory/minpoly.lean

added theorem minpoly.eq_of_irreducible

added theorem minpoly.eq_of_irreducible_of_monic

deleted theorem minpoly.unique''

deleted theorem minpoly.unique'

Modified src/ring_theory/derivation.lean

Modified src/ring_theory/polynomial_algebra.lean