Theorem Module.Dual.eq_of_preReflection_mapsTo

Modification history

2026-01-13 19:40
Mathlib/LinearAlgebra/Reflection.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …
Modified Module.Dual.eq_of_preReflection_mapsToView on Github →
2023-12-12 11:45
Mathlib/LinearAlgebra/Reflection.lean
feat: definition of reflections and root system uniqueness lemma (#8981)
Added Module.Dual.eq_of_preReflection_mapsToView on Github →