Commit 2025-03-31 10:57 25dad49b

View on Github →

feat: add a criterion for a set of roots to span an irreducible root system (#23409) The headline item is RootPairing.span_root_image_eq_top_of_forall_orthogonal.

Estimated changes

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

added theorem Submodule.smul_mem_iff''

Modified Mathlib/LinearAlgebra/Reflection.lean

added theorem Submodule.mem_invtSubmodule_reflection_of_mem

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

added theorem RootPairing.IsOrthogonal.coreflection_apply_left

added theorem RootPairing.IsOrthogonal.coreflection_apply_right

added theorem RootPairing.IsOrthogonal.flip

added theorem RootPairing.IsOrthogonal.reflection_apply_left

added theorem RootPairing.IsOrthogonal.reflection_apply_right

modified theorem RootPairing.IsOrthogonal.symm

added theorem RootPairing.isFixedPt_reflection_of_isOrthogonal

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

added theorem RootPairing.InvariantForm.apply_eq_or_of_apply_ne

Modified Mathlib/LinearAlgebra/RootSystem/Irreducible.lean

added theorem RootPairing.span_root_image_eq_top_of_forall_orthogonal