Commit 2025-03-02 22:57 9a28cbf2

View on Github →

chore: cleanup another erw by generalizing Equiv.range_eq_univ to EquivLike (#21710)

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

modified theorem AffineEquiv.range_eq

Modified Mathlib/Logic/Equiv/Set.lean

modified theorem Equiv.range_eq_univ

added theorem EquivLike.range_eq_univ

Modified Mathlib/Order/RelIso/Set.lean

modified theorem RelIso.range_eq

Modified Mathlib/RingTheory/Adjoin/Basic.lean

Modified Mathlib/Topology/Homeomorph.lean

modified theorem Homeomorph.range_coe

Modified Mathlib/Topology/MetricSpace/Isometry.lean

modified theorem IsometryEquiv.range_eq_univ

Modified Mathlib/Topology/UniformSpace/Equiv.lean

modified theorem UniformEquiv.range_coe