Commit 2023-12-12 11:45 669cc3a0

View on Github →

feat: definition of reflections and root system uniqueness lemma (#8981)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/FiniteSpan.lean

added theorem LinearEquiv.isOfFinOrder_of_finite_of_span_eq_top_of_mapsTo

Created Mathlib/LinearAlgebra/Reflection.lean

added theorem Module.Dual.eq_of_preReflection_mapsTo'

added theorem Module.Dual.eq_of_preReflection_mapsTo

added theorem Module.involutive_preReflection

added theorem Module.involutive_reflection

added def Module.preReflection

added theorem Module.preReflection_apply

added theorem Module.preReflection_apply_self

added theorem Module.preReflection_preReflection

added def Module.reflection

added theorem Module.reflection_apply

added theorem Module.reflection_apply_self

added theorem Module.reflection_symm