Commit 2024-12-10 02:59 64f35600

View on Github →

chore: address and delete many porting notes across the library (#19685)

Estimated changes

Modified Archive/Imo/Imo1972Q5.lean

Modified Archive/Imo/Imo2013Q1.lean

Modified Archive/MiuLanguage/DecisionNec.lean

Modified Archive/MiuLanguage/DecisionSuf.lean

Modified Mathlib/Algebra/AddTorsor.lean

Modified Mathlib/Algebra/BigOperators/Finsupp.lean

Modified Mathlib/Algebra/BigOperators/Group/Finset.lean

Modified Mathlib/Algebra/BigOperators/Group/Multiset.lean

Modified Mathlib/Algebra/Category/Grp/Colimits.lean

Modified Mathlib/Algebra/Category/Grp/EquivalenceGroupAddGroup.lean

Modified Mathlib/Algebra/CubicDiscriminant.lean

Modified Mathlib/Algebra/DirectLimit.lean

Modified Mathlib/Algebra/GeomSum.lean

Modified Mathlib/Algebra/Lie/Submodule.lean

Modified Mathlib/Algebra/Quandle.lean

Modified Mathlib/Algebra/Quaternion.lean

Modified Mathlib/Analysis/Normed/Lp/LpEquiv.lean

Modified Mathlib/CategoryTheory/Bicategory/Functor/Prelax.lean

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

Modified Mathlib/Data/List/DropRight.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/GroupTheory/GroupAction/Hom.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean

Modified Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

Modified Mathlib/RingTheory/WittVector/IsPoly.lean

deleted theorem WittVector.IsPoly₂.compLeft

deleted theorem WittVector.IsPoly₂.compRight

Modified Mathlib/Topology/Gluing.lean

modified theorem TopCat.GlueData.open_image_open

Modified Mathlib/Topology/UniformSpace/Completion.lean