Commit 2025-09-15 12:07 966d3cf3

View on Github →

chore: generalize AffineSubspace.isClosed_direction_iff to IsTopologicalAddTorsor (#29619)

Estimated changes

Modified Mathlib/Analysis/Complex/AbsMax.lean

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

deleted theorem AffineSubspace.isClosed_direction_iff

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

Modified Mathlib/Analysis/Normed/Module/FiniteDimension.lean

Modified Mathlib/Analysis/RCLike/Lemmas.lean

Modified Mathlib/Geometry/Euclidean/Triangle.lean

Modified Mathlib/Topology/Algebra/AffineSubspace.lean

added theorem AffineSubspace.isClosed_direction_iff