Commit 2025-12-08 18:59 323a70da

View on Github →

feat(LinearAlgebra/GeneralLinearGroup): algebra automorphisms in endomorphisms are inner (#28100) Characterization of automorphisms in endomorphisms of vector spaces: for any algebra automorphism f : End R V ≃ₐ[R] End R V, there exists a linear isomorphism T such that f a = T.conj a = T ∘ a ∘ T.symm for all a. This does not suppose finite-dimensionality. Also moves LinearAlgebra/GeneralLinearGroup to LinearAlgebra/GeneralLinearGroup/Basic.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Equiv.lean

added def LinearEquiv.conjAlgEquiv

added theorem LinearEquiv.conjAlgEquiv_apply

added theorem LinearEquiv.symm_conjAlgEquiv

Modified Mathlib/Algebra/Azumaya/Basic.lean

Modified Mathlib/Algebra/Module/LinearMap/End.lean

modified theorem LinearMap.smulRightₗ_apply

added theorem LinearMap.smulRightₗ_apply_apply

Modified Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

Modified Mathlib/LinearAlgebra/Determinant.lean

Modified Mathlib/LinearAlgebra/Dual/Lemmas.lean

added theorem Module.Projective.exists_dual_eq_one

added theorem Module.Projective.exists_dual_ne_zero

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

Created Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.lean

Renamed Mathlib/LinearAlgebra/GeneralLinearGroup.lean to Mathlib/LinearAlgebra/GeneralLinearGroup/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

deleted def LinearEquiv.algConj

Modified Mathlib/LinearAlgebra/Projection.lean

Modified Mathlib/LinearAlgebra/SpecialLinearGroup.lean

Modified Mathlib/LinearAlgebra/UnitaryGroup.lean

Modified Mathlib/NumberTheory/Modular.lean

Modified Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean