Commit 2023-08-14 19:43 1377815e

View on Github →

feat(Algebra/Algebra/Opposite): A ≃ₐ[R] Aᵐᵒᵖᵐᵒᵖ and (A ≃ₐ[R] Bᵐᵒᵖ) ≃ (Aᵐᵒᵖ ≃ₐ[R] B) (#6525) This also adds the missing AlgEquiv.equivCongr as a more general version of AlgEquiv.autCongr.

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

modified def AlgEquiv.arrowCongr

modified theorem AlgEquiv.arrowCongr_comp

modified theorem AlgEquiv.arrowCongr_symm

modified theorem AlgEquiv.arrowCongr_trans

added def AlgEquiv.equivCongr

added theorem AlgEquiv.equivCongr_refl

added theorem AlgEquiv.equivCongr_symm

added theorem AlgEquiv.equivCongr_trans

deleted theorem AlgEquiv.toLinearEquiv_apply

Modified Mathlib/Algebra/Algebra/Opposite.lean

added def AlgEquiv.opComm

added def AlgEquiv.opOp

added theorem AlgEquiv.toRingEquiv_opOp

added def AlgHom.opComm

Modified Mathlib/Algebra/Group/Opposite.lean

added def MulEquiv.opOp

Modified Mathlib/Algebra/Ring/Equiv.lean

added def RingEquiv.opOp