Commit 2025-02-10 05:14 63fc01a2

View on Github →

feat: more symm_bijectives (#21435) This extends an established pattern.

Estimated changes

Modified Mathlib/Algebra/Group/Action/Equidecomp.lean

added theorem Equidecomp.symm_bijective

added theorem Equidecomp.symm_involutive

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

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

added theorem AffineIsometryEquiv.symm_bijective

Modified Mathlib/Analysis/Normed/Operator/LinearIsometry.lean

added theorem LinearIsometryEquiv.symm_bijective

Modified Mathlib/CategoryTheory/Iso.lean

added theorem CategoryTheory.Iso.symm_bijective

Modified Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean

added theorem ContinuousAffineEquiv.symm_bijective

Modified Mathlib/ModelTheory/Basic.lean

added theorem FirstOrder.Language.Equiv.symm_bijective

Modified Mathlib/ModelTheory/PartialEquiv.lean

added theorem FirstOrder.Language.PartialEquiv.symm_bijective

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

added theorem ContinuousAlgEquiv.symm_bijective

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

added theorem ContinuousMulEquiv.symm_bijective

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

added theorem ContinuousLinearEquiv.symm_bijective