Theorem RootPairing.smul_coroot_eq_of_root_add_root_eq

Modification history

2026-01-13 19:40
Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …
Modified RootPairing.smul_coroot_eq_of_root_add_root_eqView on Github →
2025-11-17 10:36
Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean
feat: miscellaneous root system lemmas (#29147)
Added RootPairing.smul_coroot_eq_of_root_add_root_eqView on Github →