Commit 2026-11-10 19:35 2b814700

View on Github →

feat: use IsApply for AffineMap and AffineIsometry (#45599) In Analysis.Convex.PathConnected, I have to write _root_.add_apply because there is a conflict with Path.add_apply. I don't know how to make Path.add_apply protected because it is an automatically generated lemma.

Estimated changes

Modified Mathlib/Analysis/Convex/PathConnected.lean

Modified Mathlib/Analysis/Normed/Affine/Isometry.lean

added theorem AffineIsometry.toAffineMap_mul

added theorem AffineIsometry.toAffineMap_one

added theorem AffineIsometry.toAffineMap_pow

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/RingInverseOrder.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

added theorem AffineMap.mul_linear

added theorem AffineMap.one_linear

added theorem AffineMap.pow_linear

deleted theorem AffineMap.vadd_apply

Modified Mathlib/Topology/Path.lean

deleted def Path.inv