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_mapsTo'View 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_mapsTo'View on Github →