Theorem Module.eq_of_mapsTo_reflection_of_mem

Modification history

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