Commit 2025-11-26 08:20 26d3df12

View on Github →

feat(LinearAlgebra/SymmetricAlgebra): IsSymmetricAlgebra (#27308) This PR continues the work from #24602. Original PR: https://github.com/leanprover-community/mathlib4/pull/24602

Estimated changes

Modified Mathlib/LinearAlgebra/SymmetricAlgebra/Basic.lean

added theorem IsSymmetricAlgebra.algHom_ext

added theorem IsSymmetricAlgebra.comp_equiv

added theorem IsSymmetricAlgebra.equiv_apply

added theorem IsSymmetricAlgebra.equiv_symm_apply

added theorem IsSymmetricAlgebra.equiv_symm_comp

added theorem IsSymmetricAlgebra.equiv_toAlgHom

added theorem IsSymmetricAlgebra.induction

added theorem IsSymmetricAlgebra.lift_comp_linearMap

added theorem IsSymmetricAlgebra.lift_eq

added theorem IsSymmetricAlgebra.lift_unique

added theorem IsSymmetricAlgebra.of_equiv

added def IsSymmetricAlgebra

added theorem SymmetricAlgebra.isSymmetricAlgebra_ι

Modified Mathlib/LinearAlgebra/SymmetricAlgebra/Basis.lean

added theorem SymmetricAlgebra.IsSymmetricAlgebra.mvPolynomial