Theorem CharZero.of_noZeroSMulDivisors

Modification history

2026-01-13 19:40
Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …
Deleted CharZero.of_noZeroSMulDivisorsView on Github →
2025-11-05 11:15
Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean
chore: use `IsAddTorsionFree M` instead of `NoZeroSMulDivisors ℕ M`/`NoZeroSMulDivisors ℤ M` (#30683) …
Modified CharZero.of_noZeroSMulDivisorsView on Github →
2024-10-19 07:30
Mathlib/Algebra/Module/Defs.lean
chore(Algebra/Module): split off `NoZeroSMulDivisors` (#17909) …
Modified CharZero.of_noZeroSMulDivisorsView on Github →
2024-04-29 13:25
Mathlib/Algebra/Module/Basic.lean
chore: split Algebra.Module.Basic (#12501) …
Modified CharZero.of_noZeroSMulDivisorsView on Github →
2023-12-11 22:56
Mathlib/Algebra/Module/Basic.lean
feat: supporting lemmas for defining root systems (#8980) …
Added CharZero.of_noZeroSMulDivisorsView on Github →