Commit 2024-08-07 13:48 b9905c84

View on Github →

chore: backports for leanprover/lean4#4814 (part 26) (#15538)

Estimated changes

Modified Mathlib/Algebra/Jordan/Basic.lean

modified theorem two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add

Modified Mathlib/Algebra/Lie/CartanMatrix.lean

modified def CartanMatrix.Relations.EF

modified def CartanMatrix.Relations.toIdeal

modified def CartanMatrix.Relations.toSet

Modified Mathlib/Algebra/Lie/IdealOperations.lean

modified theorem LieSubmodule.comap_bracket_eq

modified theorem LieSubmodule.lieIdeal_oper_eq_linear_span'

modified theorem LieSubmodule.lieIdeal_oper_eq_linear_span

modified theorem LieSubmodule.map_bracket_eq

Modified Mathlib/Algebra/Lie/Nilpotent.lean

modified theorem LieIdeal.coe_lcs_eq

modified theorem LieModule.lowerCentralSeriesLast_le_max_triv

Modified Mathlib/Algebra/Lie/Quotient.lean

Modified Mathlib/Analysis/InnerProductSpace/Spectrum.lean

modified theorem LinearMap.IsSymmetric.conj_eigenvalue_eq_self

modified theorem LinearMap.IsSymmetric.direct_sum_isInternal

modified theorem LinearMap.IsSymmetric.invariant_orthogonalComplement_eigenspace

modified theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces

modified theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot'

modified theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot

modified theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_invariant

modified theorem LinearMap.IsSymmetric.orthogonalFamily_eigenspaces'

modified theorem LinearMap.IsSymmetric.orthogonalFamily_eigenspaces

Modified Mathlib/Analysis/Normed/Lp/PiLp.lean

modified theorem PiLp.nnnorm_equiv_symm_single

Modified Mathlib/FieldTheory/Laurent.lean

Modified Mathlib/FieldTheory/Normal.lean

modified theorem AlgHom.fieldRange_of_normal

Modified Mathlib/LinearAlgebra/JordanChevalley.lean

Modified Mathlib/NumberTheory/RamificationInertia.lean

modified theorem Ideal.Quotient.algebraMap_quotient_of_ramificationIdx_neZero

modified def Ideal.Quotient.algebraQuotientOfRamificationIdxNeZero

Modified Mathlib/RepresentationTheory/Character.lean