Commit 2023-12-01 11:18 e368f2a5

View on Github →

feat(/Equiv/): Add symm_bijective lemmas next to symm_symms (#8444)

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

Modified Mathlib/Algebra/Group/Equiv/Basic.lean

modified theorem MulEquiv.symm_bijective

Modified Mathlib/Algebra/Homology/ComplexShape.lean

added theorem ComplexShape.symm_bijective

Modified Mathlib/Algebra/Lie/Basic.lean

added theorem LieEquiv.symm_bijective

added theorem LieModuleEquiv.symm_bijective

Modified Mathlib/Algebra/Module/Equiv.lean

Modified Mathlib/Algebra/Order/Hom/Ring.lean

modified theorem OrderRingIso.symm_bijective

Modified Mathlib/Algebra/Ring/Equiv.lean

modified theorem RingEquiv.symm_bijective

Modified Mathlib/Algebra/Star/StarAlgHom.lean

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

Modified Mathlib/Data/PEquiv.lean

added theorem PEquiv.symm_bijective

Modified Mathlib/Logic/Equiv/Defs.lean

added theorem Equiv.symm_bijective

Modified Mathlib/Logic/Equiv/LocalEquiv.lean

added theorem LocalEquiv.symm_bijective

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

added theorem MeasurableEquiv.symm_bijective

Modified Mathlib/Order/Hom/Basic.lean

added theorem OrderIso.symm_bijective

modified theorem OrderIso.symm_injective

Modified Mathlib/Topology/Connected/PathConnected.lean

added theorem Path.symm_bijective

modified theorem Path.symm_symm

Modified Mathlib/Topology/Homeomorph.lean

added theorem Homeomorph.symm_bijective

Modified Mathlib/Topology/Homotopy/Basic.lean

added theorem ContinuousMap.Homotopy.symm_bijective

added theorem ContinuousMap.HomotopyRel.symm_bijective

added theorem ContinuousMap.HomotopyWith.symm_bijective

Modified Mathlib/Topology/Homotopy/Path.lean

added theorem Path.Homotopy.symm_bijective

Modified Mathlib/Topology/LocalHomeomorph.lean

added theorem LocalHomeomorph.symm_bijective

Modified Mathlib/Topology/MetricSpace/DilationEquiv.lean

added theorem DilationEquiv.symm_bijective

Modified Mathlib/Topology/MetricSpace/Isometry.lean

added theorem IsometryEquiv.symm_bijective

Modified Mathlib/Topology/UnitInterval.lean

added theorem unitInterval.symm_bijective