Commit 2025-04-21 11:55 9da3d905

View on Github →

feat(LinearAlgebra/RootSystem): Characterize root system invariant submodules in terms of roots (#23945) Characterize root system invariant submodules in terms of roots

Estimated changes

Modified Mathlib/LinearAlgebra/Dual/Lemmas.lean

added theorem Submodule.dualCoannihilator_top

deleted theorem Subspace.dualCoannihilator_top

Modified Mathlib/LinearAlgebra/Reflection.lean

added theorem Submodule.mem_invtSubmodule_reflection_iff

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

deleted theorem RootPairing.coe_corootSpan_dualAnnihilator_map

deleted theorem RootPairing.coe_rootSpan_dualAnnihilator_map

added theorem RootPairing.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot'

added theorem RootPairing.corootSpan_map_toDualRight

added theorem RootPairing.iInf_ker_coroot'_eq

added theorem RootPairing.iInf_ker_root'_eq

added theorem RootPairing.rootSpan_dualAnnihilator_map_eq_iInf_ker_root'

added theorem RootPairing.rootSpan_map_toDualLeft

added theorem RootPairing.span_coroot'_eq_top

added theorem RootPairing.span_root'_eq_top

added theorem RootPairing.toDualLeft_comp_root

added theorem RootPairing.toDualRight_comp_root

Modified Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean

Modified Mathlib/LinearAlgebra/RootSystem/Irreducible.lean

added theorem RootPairing.exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule

added theorem RootSystem.eq_top_of_mem_invtSubmodule_of_forall_eq_univ