Theorem ContinuousAffineMap.to_affine_map_contLinear

Modification history

2025-09-23 19:02

Mathlib/Analysis/Normed/Affine/ContinuousAffineMap.lean

chore: generalize `ContinuousAffineMap.contLinear` to `IsTopologicalAddTorsor` (#29617)

Deleted ContinuousAffineMap.to_affine_map_contLinear View on Github →

2023-06-09 09:11

Mathlib/Analysis/NormedSpace/ContinuousAffineMap.lean

feat: port Analysis.NormedSpace.ContinuousAffineMap (#4867)

Added ContinuousAffineMap.to_affine_map_contLinear View on Github →