Commit 2026-06-24 17:13 b5f56a63

View on Github →

feat(Mathlib.Topology.Algebra.Module.Equiv): add results on IsHomeomorph (#39476) Add the construction of a ContinuousLinearEquiv from a LinearEquiv that IsHomeomorph, and two basic API lemmas. Also remove a simp tag from a lemma in about Function.Bijective, and change its signature a bit.

Estimated changes

Modified Mathlib/Topology/Algebra/Module/Equiv.lean

added theorem ContinuousLinearEquiv.coe_ofIsHomeomorph

added theorem ContinuousLinearEquiv.isHomeomorph

added def ContinuousLinearEquiv.ofIsHomeomorph

added theorem ContinuousLinearEquiv.toLinearquiv_ofIsHomeomorph

modified theorem LinearEquiv.isHomeomorph_iff