Commit 2023-04-02 23:34 bb7d4c76

View on Github →

chore: tidy various files (#3233)

Estimated changes

Modified Mathlib/Analysis/Convex/Extreme.lean

Modified Mathlib/CategoryTheory/Elements.lean

modified def CategoryTheory.CategoryOfElements.fromCostructuredArrow

modified def CategoryTheory.CategoryOfElements.fromStructuredArrow

modified def CategoryTheory.CategoryOfElements.toStructuredArrow

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/MvPolynomial/Division.lean

added theorem MvPolynomial.X_divMonomial

added theorem MvPolynomial.X_dvd_X

added theorem MvPolynomial.X_dvd_iff_modMonomial_eq_zero

added theorem MvPolynomial.X_dvd_monomial

added theorem MvPolynomial.X_mul_divMonomial

added theorem MvPolynomial.X_mul_modMonomial

added theorem MvPolynomial.modMonomial_X

deleted theorem MvPolynomial.modMonomial_x

added theorem MvPolynomial.mul_X_divMonomial

added theorem MvPolynomial.mul_X_modMonomial

deleted theorem MvPolynomial.mul_x_divMonomial

deleted theorem MvPolynomial.mul_x_modMonomial

deleted theorem MvPolynomial.x_divMonomial

deleted theorem MvPolynomial.x_dvd_iff_modMonomial_eq_zero

deleted theorem MvPolynomial.x_dvd_monomial

deleted theorem MvPolynomial.x_dvd_x

deleted theorem MvPolynomial.x_mul_divMonomial

deleted theorem MvPolynomial.x_mul_modMonomial

Modified Mathlib/Data/Nat/Factorization/Basic.lean

Modified Mathlib/Data/Nat/Totient.lean

deleted theorem Nat.card_units_zMod_lt_sub_one

added theorem Nat.card_units_zmod_lt_sub_one

Modified Mathlib/Data/Polynomial/FieldDivision.lean

deleted theorem Polynomial.divByMonic_add_X_Sub_C_mul_derivate_divByMonic_eq_derivative

added theorem Polynomial.divByMonic_add_X_sub_C_mul_derivate_divByMonic_eq_derivative

modified theorem Polynomial.map_div

added theorem Polynomial.mod_X_sub_C_eq_C_eval

deleted theorem Polynomial.mod_x_sub_c_eq_c_eval

added theorem Polynomial.not_irreducible_C

deleted theorem Polynomial.not_irreducible_c

Modified Mathlib/Data/Polynomial/Mirror.lean

Modified Mathlib/NumberTheory/LucasPrimality.lean

Modified Mathlib/RingTheory/Polynomial/Vieta.lean

Modified Mathlib/Topology/Algebra/Polynomial.lean