Commit 2025-09-16 17:10 076512b2

View on Github →

chore(Topology/Algebra/Affine): generalize to IsTopologicalAddTorsor (#29616)

Estimated changes

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

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

deleted theorem AffineMap.continuous_linear_iff

deleted theorem AffineMap.isOpenMap_linear_iff

Modified Mathlib/Analysis/Normed/Operator/Banach.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

added theorem AffineMap.coe_homothety

Modified Mathlib/Topology/Algebra/Affine.lean

modified theorem AffineMap.continuous_iff

added theorem AffineMap.continuous_linear_iff

modified theorem AffineMap.homothety_continuous

modified theorem AffineMap.homothety_isOpenMap

added theorem AffineMap.isOpenMap_linear_iff

modified theorem AffineMap.lineMap_continuous