Commit 2025-07-15 08:11 1164c0de

View on Github →

feat: semilinearize LinearEquiv.conjRingEquiv (#27104)

Estimated changes

Modified Mathlib/Algebra/Lie/OfAssociative.lean

modified theorem LieAlgebra.conj_ad_apply

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

modified def LinearEquiv.arrowCongr

modified def LinearEquiv.arrowCongrAddEquiv

modified theorem LinearEquiv.arrowCongr_apply

modified theorem LinearEquiv.arrowCongr_comp

modified theorem LinearEquiv.arrowCongr_symm_apply

modified theorem LinearEquiv.arrowCongr_trans

modified def LinearEquiv.conj

modified def LinearEquiv.conjRingEquiv

modified theorem LinearEquiv.conj_apply

modified theorem LinearEquiv.conj_apply_apply

modified theorem LinearEquiv.conj_comp

modified theorem LinearEquiv.conj_conj_symm

modified theorem LinearEquiv.conj_id

modified theorem LinearEquiv.conj_symm_conj

modified theorem LinearEquiv.conj_trans

modified def LinearEquiv.domMulActCongrRight

modified theorem LinearEquiv.symm_conj_apply

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean