Commit 2025-03-11 13:02 dd1ab1e8

View on Github →

feat: define irreducible root systems / pairings (#22803)

Estimated changes

Modified Mathlib.lean

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

added theorem LinearEquiv.conj_refl

Modified Mathlib/Algebra/Module/Submodule/Invariant.lean

added theorem LinearEquiv.map_mem_invtSubmodule_conj_iff

added theorem LinearEquiv.map_mem_invtSubmodule_iff

added theorem Module.End.span_orbit_mem_invtSubmodule

Modified Mathlib/Algebra/Module/Submodule/Map.lean

Modified Mathlib/GroupTheory/GroupAction/Defs.lean

added theorem MulAction.mem_orbit_of_mem_orbit

Modified Mathlib/LinearAlgebra/Dual/Defs.lean

added theorem Submodule.dualAnnihilator_map_dualMap_le

Modified Mathlib/LinearAlgebra/Dual/Lemmas.lean

added theorem Submodule.dualAnnihilator_eq_bot_iff'

added theorem Submodule.dualAnnihilator_eq_bot_iff

added theorem Submodule.dualAnnihilator_eq_top_iff

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

added theorem RootPairing.corootSpan_mem_invtSubmodule_coreflection

added theorem RootPairing.corootSpan_ne_bot

added theorem RootPairing.exists_ne_zero'

added theorem RootPairing.exists_ne_zero

added theorem RootPairing.rootSpan_mem_invtSubmodule_reflection

added theorem RootPairing.rootSpan_ne_bot

added theorem RootPairing.toDualLeft_conj_reflection

added theorem RootPairing.toDualRight_conj_coreflection

Modified Mathlib/LinearAlgebra/RootSystem/Hom.lean

Created Mathlib/LinearAlgebra/RootSystem/Irreducible.lean

added theorem RootPairing.IsIrreducible.mk'

added theorem RootPairing.invtSubmodule_reflection_of_invtSubmodule_coreflection

added theorem RootPairing.isSimpleModule_weylGroupRootRep

added theorem RootPairing.isSimpleModule_weylGroupRootRep_iff

added theorem RootPairing.span_orbit_eq_top

added def RootPairing.toRootSystem

Modified Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean

added theorem RootPairing.weylGroup.induction'

added theorem RootPairing.weylGroup.induction

added def RootPairing.weylGroupCorootRep

added def RootPairing.weylGroupRootRep

added theorem RootPairing.weylGroup_toSubmonoid

Modified Mathlib/LinearAlgebra/Span/Defs.lean

modified theorem Submodule.span_singleton_eq_bot

Modified Mathlib/RepresentationTheory/Basic.lean

modified theorem Representation.asAlgebraHom_single

modified theorem Representation.asAlgebraHom_single_one

modified def Representation.asModuleEquiv

added theorem Representation.single_smul

Modified Mathlib/RepresentationTheory/Rep.lean

Created Mathlib/RepresentationTheory/Submodule.lean

added theorem Representation.asAlgebraHom_mem_of_forall_mem

added def Representation.invtSubmodule

added def Representation.mapSubmodule

added theorem Representation.mem_invtSubmodule