Theorem Module.infinite_range_reflection_reflection_iterate_iff

Modification history

2025-11-05 11:15

Mathlib/LinearAlgebra/Reflection.lean

chore: use `IsAddTorsionFree M` instead of `NoZeroSMulDivisors ℕ M`/`NoZeroSMulDivisors ℤ M` (#30683) …

Modified Module.infinite_range_reflection_reflection_iterate_iff View on Github →

2024-08-10 20:14

Mathlib/LinearAlgebra/Reflection.lean

feat (LinearAlgebra/RootSystem) : infinitely many roots when two are parallel (#15582) …

Added Module.infinite_range_reflection_reflection_iterate_iff View on Github →