Commit 2025-02-20 15:30 55df44f2

View on Github →

chore: rename ContMDiff.sum_{elim,map} (#22131)

Estimated changes

Modified Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean

added theorem ContMDiff.sumElim

added theorem ContMDiff.sumMap

deleted theorem ContMDiff.sum_elim

deleted theorem ContMDiff.sum_map

modified theorem ContMDiff.swap