Theorem Module.eq_of_mapsTo_reflection_of_mem

Modification history

2026-09-30 14:37
Mathlib/LinearAlgebra/Reflection.lean
refactor(Algebra/Group): fix the definition of torsion-free non-abelian groups (#42407) …
Modified Module.eq_of_mapsTo_reflection_of_memView on Github →
2025-11-05 11:15
Mathlib/LinearAlgebra/Reflection.lean
chore: use `IsAddTorsionFree M` instead of `NoZeroSMulDivisors ℕ M`/`NoZeroSMulDivisors ℤ M` (#30683) …
Modified Module.eq_of_mapsTo_reflection_of_memView on Github →
2024-06-28 20:06
Mathlib/LinearAlgebra/Reflection.lean
refactor (LinearAlgebra/RootSystem) : change definition of RootPairing (#13917) …
Added Module.eq_of_mapsTo_reflection_of_memView on Github →