Commit 2024-12-28 23:51 1a402974

View on Github →

chore: rename update_same/update_noteq to update_self/update_of_ne (#20302) The previous names didn't match the naming convention

Estimated changes

Modified Mathlib/Algebra/Group/Pi/Basic.lean

Modified Mathlib/Algebra/Group/Pi/Lemmas.lean

Modified Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean

Modified Mathlib/Algebra/Group/Subgroup/Finite.lean

Modified Mathlib/Algebra/Group/TypeTags/Basic.lean

Modified Mathlib/Algebra/Order/Antidiag/Finsupp.lean

Modified Mathlib/Analysis/Analytic/Composition.lean

Modified Mathlib/Analysis/BoxIntegral/Partition/Additive.lean

Modified Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean

Modified Mathlib/Analysis/Calculus/DSlope.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

Modified Mathlib/Analysis/Complex/CauchyIntegral.lean

Modified Mathlib/Analysis/Complex/Periodic.lean

Modified Mathlib/Analysis/Convex/Extreme.lean

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

Modified Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean

Modified Mathlib/CategoryTheory/Filtered/Final.lean

Modified Mathlib/Computability/TMToPartrec.lean

Modified Mathlib/Computability/TuringMachine.lean

Modified Mathlib/Data/DFinsupp/Defs.lean

Modified Mathlib/Data/Fin/Tuple/Basic.lean

Modified Mathlib/Data/Fin/Tuple/Take.lean

Modified Mathlib/Data/Finset/PiInduction.lean

Modified Mathlib/Data/Finset/Piecewise.lean

Modified Mathlib/Data/Finset/Update.lean

Modified Mathlib/Data/Finsupp/Defs.lean

Modified Mathlib/Data/Fintype/Prod.lean

Modified Mathlib/Data/Matrix/RowCol.lean

Modified Mathlib/Data/Nat/Choose/Multinomial.lean

Modified Mathlib/Data/Set/Card.lean

Modified Mathlib/Data/Set/Lattice.lean

Modified Mathlib/Data/Set/Prod.lean

Modified Mathlib/Data/Sigma/Basic.lean

Modified Mathlib/Data/Sum/Basic.lean

Modified Mathlib/Geometry/Manifold/Instances/Real.lean

Modified Mathlib/GroupTheory/Complement.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Combination.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

Modified Mathlib/LinearAlgebra/Alternating/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/Basis.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

Modified Mathlib/LinearAlgebra/Pi.lean

Modified Mathlib/LinearAlgebra/PiTensorProduct.lean

Modified Mathlib/Logic/Equiv/Basic.lean

Modified Mathlib/Logic/Function/Basic.lean

deleted theorem Function.update_noteq

added theorem Function.update_of_ne

deleted theorem Function.update_same

added theorem Function.update_self

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

Modified Mathlib/MeasureTheory/Integral/FundThmCalculus.lean

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

Modified Mathlib/MeasureTheory/Integral/Marginal.lean

Modified Mathlib/NumberTheory/LSeries/DirichletContinuation.lean

Modified Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean

Modified Mathlib/NumberTheory/LSeries/Nonvanishing.lean

Modified Mathlib/NumberTheory/LSeries/PrimesInAP.lean

Modified Mathlib/NumberTheory/LSeries/RiemannZeta.lean

Modified Mathlib/NumberTheory/LSeries/ZMod.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean

Modified Mathlib/Order/Atoms.lean

Modified Mathlib/Order/Basic.lean

Modified Mathlib/Order/Bounds/Image.lean

Modified Mathlib/Order/CompleteLattice/Finset.lean

Modified Mathlib/Order/Interval/Set/Pi.lean

Modified Mathlib/Order/Lattice.lean

Modified Mathlib/Order/PiLex.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

Modified Mathlib/RingTheory/Localization/Basic.lean

Modified Mathlib/RingTheory/MaximalSpectrum.lean

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

Modified Mathlib/RingTheory/PrimeSpectrum.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Group.lean

Modified Mathlib/Topology/Algebra/Module/Multilinear/Bounded.lean

Modified Mathlib/Topology/Algebra/WithZeroTopology.lean

Modified Mathlib/Topology/ContinuousOn.lean

Modified Mathlib/Topology/Order.lean

Modified Mathlib/Topology/Separation/Basic.lean

Modified Mathlib/Topology/ShrinkingLemma.lean