Commit 2025-09-17 13:39 47146f09

View on Github →

chore(Topology/Algebra/Affine): generalize eventually_homothety_* to IsTopologicalAddTorsor (#29620)

Estimated changes

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

deleted theorem eventually_homothety_image_subset_of_finite_subset_interior

deleted theorem eventually_homothety_mem_of_mem_interior

Modified Mathlib/Topology/Algebra/Affine.lean

added theorem eventually_homothety_image_subset_of_finite_subset_interior

added theorem eventually_homothety_mem_of_mem_interior