Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-08-03 10:01
484c019b
View on Github →
chore: remove some uses of
open Classical
, part 2 (
#15413
) See
#15371
.
Estimated changes
Modified
Mathlib/Algebra/Category/AlgebraCat/Basic.lean
Modified
Mathlib/Algebra/Category/AlgebraCat/Limits.lean
Modified
Mathlib/Algebra/Category/FGModuleCat/Basic.lean
Modified
Mathlib/Algebra/Category/FGModuleCat/Limits.lean
Modified
Mathlib/Algebra/Category/Grp/Adjunctions.lean
Modified
Mathlib/Algebra/Category/Grp/FilteredColimits.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
Modified
Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean
Modified
Mathlib/Algebra/Category/MonCat/FilteredColimits.lean
Modified
Mathlib/Algebra/Category/Ring/Adjunctions.lean
Modified
Mathlib/Algebra/Category/Ring/Colimits.lean
Modified
Mathlib/Algebra/Category/Ring/Constructions.lean
Modified
Mathlib/Algebra/Category/Ring/FilteredColimits.lean
Modified
Mathlib/Algebra/EuclideanDomain/Defs.lean
Modified
Mathlib/Algebra/Field/IsField.lean
Modified
Mathlib/Algebra/Group/Subgroup/Basic.lean
Modified
Mathlib/Algebra/GroupWithZero/Basic.lean
modified
theorem
mul_eq_zero_of_ne_zero_imp_eq_zero
Modified
Mathlib/Algebra/GroupWithZero/Commute.lean
Modified
Mathlib/Algebra/GroupWithZero/Units/Basic.lean
Modified
Mathlib/Algebra/Homology/ComplexShape.lean
Modified
Mathlib/Algebra/Homology/DifferentialObject.lean
Modified
Mathlib/Algebra/Homology/Homotopy.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory.lean
Modified
Mathlib/Algebra/Homology/ImageToKernel.lean
Modified
Mathlib/Algebra/Module/DedekindDomain.lean
modified
theorem
Submodule.isInternal_prime_power_torsion
modified
theorem
Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal
Modified
Mathlib/Algebra/Module/PID.lean
modified
theorem
Submodule.isInternal_prime_power_torsion_of_pid
Modified
Mathlib/Algebra/MonoidAlgebra/Degree.lean
modified
theorem
AddMonoidAlgebra.sup_support_add_le
Modified
Mathlib/Algebra/MvPolynomial/Rename.lean
Modified
Mathlib/Algebra/Order/CauSeq/Completion.lean
Modified
Mathlib/Algebra/Order/CompleteField.lean
Modified
Mathlib/Algebra/Order/GroupWithZero/Synonym.lean
Modified
Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
Modified
Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
Modified
Mathlib/AlgebraicGeometry/Limits.lean
Modified
Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean
Modified
Mathlib/AlgebraicGeometry/PrimeSpectrum/Maximal.lean
Modified
Mathlib/AlgebraicGeometry/StructureSheaf.lean
Modified
Mathlib/AlgebraicTopology/TopologicalSimplex.lean
Modified
Mathlib/Analysis/Analytic/Basic.lean
Modified
Mathlib/Analysis/ConstantSpeed.lean
Modified
Mathlib/Analysis/Hofer.lean
Modified
Mathlib/Analysis/MeanInequalities.lean
Modified
Mathlib/Analysis/MeanInequalitiesPow.lean
Modified
Mathlib/Analysis/Seminorm.lean
Modified
Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
Modified
Mathlib/Dynamics/Ergodic/Conservative.lean
Modified
Mathlib/FieldTheory/AbelRuffini.lean
Modified
Mathlib/FieldTheory/Finiteness.lean
Modified
Mathlib/FieldTheory/Fixed.lean
Modified
Mathlib/FieldTheory/IsPerfectClosure.lean
Modified
Mathlib/FieldTheory/IsSepClosed.lean
Modified
Mathlib/FieldTheory/KrullTopology.lean
Modified
Mathlib/FieldTheory/Laurent.lean
Modified
Mathlib/FieldTheory/MvPolynomial.lean
Modified
Mathlib/FieldTheory/Normal.lean
Modified
Mathlib/FieldTheory/PrimitiveElement.lean
Modified
Mathlib/FieldTheory/Separable.lean
modified
theorem
Polynomial.count_roots_le_one
modified
theorem
Polynomial.multiplicity_le_one_of_separable
modified
theorem
Polynomial.nodup_roots
modified
theorem
Polynomial.separable_gcd_left
modified
theorem
Polynomial.separable_gcd_right
Modified
Mathlib/FieldTheory/SeparableClosure.lean
Modified
Mathlib/MeasureTheory/Group/Prod.lean
Modified
Mathlib/MeasureTheory/Integral/Bochner.lean
Modified
Mathlib/MeasureTheory/Integral/IntegrableOn.lean
Modified
Mathlib/MeasureTheory/Integral/Lebesgue.lean
Modified
Mathlib/MeasureTheory/Integral/Marginal.lean
Modified
Mathlib/MeasureTheory/Integral/MeanInequalities.lean
Modified
Mathlib/MeasureTheory/Integral/SetToL1.lean
modified
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_filter
Modified
Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
modified
theorem
measurableSet_insert
Modified
Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
Modified
Mathlib/MeasureTheory/Measure/AEMeasurable.lean
Modified
Mathlib/MeasureTheory/Measure/Complex.lean
Modified
Mathlib/MeasureTheory/Measure/Dirac.lean
modified
theorem
MeasureTheory.Measure.map_dirac
Modified
Mathlib/MeasureTheory/Measure/GiryMonad.lean
Modified
Mathlib/MeasureTheory/Measure/Haar/Basic.lean
Modified
Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
Modified
Mathlib/MeasureTheory/Measure/Stieltjes.lean
Modified
Mathlib/MeasureTheory/Measure/VectorMeasure.lean
Modified
Mathlib/MeasureTheory/Measure/WithDensityVectorMeasure.lean
Modified
Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
Modified
Mathlib/MeasureTheory/OuterMeasure/Induced.lean
Modified
Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
Modified
Mathlib/MeasureTheory/OuterMeasure/Operations.lean
Modified
Mathlib/RingTheory/DedekindDomain/Ideal.lean
modified
theorem
count_le_of_ideal_ge
modified
theorem
irreducible_pow_sup
modified
theorem
irreducible_pow_sup_of_ge
modified
theorem
irreducible_pow_sup_of_le
modified
theorem
sup_eq_prod_inf_factors