Commit 2023-06-25 09:03 2ac7bc89

View on Github →

chore: tidy various files (#5458)

Estimated changes

Modified Archive/Examples/PropEncodable.lean

Modified Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean

added def ModuleCat.FilteredColimits.colimitSMulAux

added theorem ModuleCat.FilteredColimits.colimitSMulAux_eq_of_rel

deleted def ModuleCat.FilteredColimits.colimitSmulAux

deleted theorem ModuleCat.FilteredColimits.colimitSmulAux_eq_of_rel

Modified Mathlib/AlgebraicGeometry/OpenImmersion/Basic.lean

modified def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoOfRangeEq

modified theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.sheafedSpace_toSheafedSpace

modified theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.to_iso

Modified Mathlib/Analysis/Complex/CauchyIntegral.lean

Modified Mathlib/Analysis/Fourier/PoissonSummation.lean

Modified Mathlib/Analysis/InnerProductSpace/Spectrum.lean

Modified Mathlib/CategoryTheory/Monoidal/Internal/Types.lean

Modified Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean

modified def CategoryTheory.symmetricOfHasFiniteCoproducts

Modified Mathlib/FieldTheory/Normal.lean

Modified Mathlib/NumberTheory/Cyclotomic/Rat.lean

Modified Mathlib/NumberTheory/NumberField/Basic.lean

Modified Mathlib/Order/Category/SemilatCat.lean

Modified Mathlib/Probability/Density.lean

Modified Mathlib/Probability/Kernel/Basic.lean

Modified Mathlib/Probability/Kernel/Condexp.lean

Modified Mathlib/Probability/Kernel/IntegralCompProd.lean

Modified Mathlib/Probability/Variance.lean

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

Modified Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean

added theorem cyclotomic_comp_X_add_one_isEisensteinAt

deleted theorem cyclotomic_comp_x_add_one_isEisensteinAt

added theorem cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt

deleted theorem cyclotomic_prime_pow_comp_x_add_one_isEisensteinAt

added theorem dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt

deleted theorem dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_is_eiseinstein_at

added theorem mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt

deleted theorem mem_adjoin_of_smul_prime_pow_smul_of_minpoly_is_eiseinstein_at

added theorem mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt

deleted theorem mem_adjoin_of_smul_prime_smul_of_minpoly_is_eiseinstein_at

Modified Mathlib/RingTheory/RingHomProperties.lean

Modified Mathlib/RingTheory/Valuation/ValuationSubring.lean

added def ValuationSubring.pointwiseHasSMul

deleted def ValuationSubring.pointwiseHasSmul