Commit 2024-09-24 16:00 067644f0

View on Github →

chore: rename Function.comp.assoc to Function.comp_assoc (#17098)

Estimated changes

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

Modified Mathlib/Algebra/Module/PID.lean

Modified Mathlib/Algebra/Order/Rearrangement.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

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

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

Modified Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean

Modified Mathlib/Analysis/Convex/Intrinsic.lean

Modified Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean

Modified Mathlib/Combinatorics/HalesJewett.lean

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

Modified Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

Modified Mathlib/Geometry/Manifold/LocalInvariantProperties.lean

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

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

Modified Mathlib/LinearAlgebra/Alternating/Basic.lean

Modified Mathlib/LinearAlgebra/Determinant.lean

Modified Mathlib/LinearAlgebra/LinearDisjoint.lean

Modified Mathlib/LinearAlgebra/Matrix/Block.lean

Modified Mathlib/LinearAlgebra/RootSystem/Hom.lean

Modified Mathlib/Logic/Function/Basic.lean

Modified Mathlib/Logic/Function/Defs.lean

deleted theorem Function.comp.assoc

added theorem Function.comp_assoc

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

Modified Mathlib/ModelTheory/Basic.lean

Modified Mathlib/ModelTheory/DirectLimit.lean

Modified Mathlib/ModelTheory/ElementaryMaps.lean

Modified Mathlib/ModelTheory/Syntax.lean

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

Modified Mathlib/Topology/Category/CompHaus/Projective.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean

Modified Mathlib/Topology/Category/Profinite/Projective.lean

Modified Mathlib/Topology/Category/TopCat/EffectiveEpi.lean

Modified Mathlib/Topology/ExtremallyDisconnected.lean

Modified Mathlib/Topology/Homeomorph.lean