Commit 2025-08-18 05:45 aca000b7

View on Github →

chore(*): process elementwise porting notes (#28403) There are a couple porting notes complaining about elementwise, but the generated lemmas look fine to me. If this PR compiles, we can just drop those notes.

Estimated changes

Modified Mathlib/Algebra/Homology/ImageToKernel.lean

deleted theorem imageToKernel_arrow_apply

Modified Mathlib/CategoryTheory/Limits/Types/Shapes.lean

deleted theorem CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval_apply

deleted theorem CategoryTheory.Limits.Types.productIso_hom_comp_eval_apply

Modified Mathlib/Geometry/RingedSpace/Stalks.lean

Modified Mathlib/Topology/Gluing.lean