Commit 2026-03-25 06:44 a1ec97cc

View on Github →

feat: affine isomorphisms between spaces of affine maps (#35998) These isomorphisms are analogous to LinearEquiv.arrowCongr and LinearEquiv.congrLeft.

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

added def AffineEquiv.arrowCongr

added def AffineEquiv.arrowCongrEquiv

added theorem AffineEquiv.arrowCongrEquiv_apply

added theorem AffineEquiv.arrowCongrEquiv_symm_apply

added theorem AffineEquiv.arrowCongr_apply

added theorem AffineEquiv.arrowCongr_symm_apply

added def AffineEquiv.arrowCongrₗ

added theorem AffineEquiv.arrowCongrₗ_apply

added theorem AffineEquiv.arrowCongrₗ_symm_apply

added def AffineEquiv.congrLeft

added theorem AffineEquiv.congrLeft_apply

added theorem AffineEquiv.congrLeft_symm_apply

added def AffineEquiv.congrLeftₗ

added theorem AffineEquiv.congrLeftₗ_apply

added theorem AffineEquiv.congrLeftₗ_symm_apply