Commit 2024-01-16 14:21 51956bca

View on Github →

chore(Analysis,Geometry): remove almost all autoImplicit (#9691) After this PR, no file in Geometry uses autoImplicit, and in Analysis it's scoped to six declarations.

Estimated changes

Modified Mathlib/Analysis/Calculus/Deriv/Star.lean

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

modified theorem HasFDerivWithinAt.of_not_mem_tsupport

Modified Mathlib/Analysis/Complex/CauchyIntegral.lean

Modified Mathlib/Analysis/Convex/Gauge.lean

Modified Mathlib/Analysis/Convex/StrictConvexSpace.lean

Modified Mathlib/Analysis/NormedSpace/lpSpace.lean

Modified Mathlib/Analysis/Seminorm.lean

modified theorem Seminorm.neg_mem_ball_zero

Modified Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

modified theorem Mathlib.Meta.Positivity.log_nonneg_of_isNat

modified theorem Mathlib.Meta.Positivity.log_nonneg_of_isNegNat

modified theorem Mathlib.Meta.Positivity.log_pos_of_isNat

modified theorem Mathlib.Meta.Positivity.log_pos_of_isNegNat

Modified Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean

modified theorem expNegInvGlue.zero_iff_nonpos

Modified Mathlib/Geometry/Euclidean/Inversion/Basic.lean

Modified Mathlib/Geometry/Euclidean/PerpBisector.lean

Modified Mathlib/Geometry/Manifold/Algebra/LieGroup.lean

Modified Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

modified theorem UniqueMDiffWithinAt.image_denseRange

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

modified theorem PartialHomeomorph.continuousWithinAt_writtenInExtend_iff

modified theorem PartialHomeomorph.tendsto_extend_comp_iff

Modified Mathlib/Geometry/Manifold/VectorBundle/Basic.lean

modified theorem contMDiffAt_coordChangeL

modified theorem smoothAt_coordChangeL