Theorem isSMulRegular_algebraMap_iff

Modification history

2026-01-12 13:34

Mathlib/Algebra/Algebra/Basic.lean

feat(Algebra): more `Module.IsTorsionFree` API (#33871) …

Modified isSMulRegular_algebraMap_iff View on Github →

2024-06-07 06:15

Mathlib/RingTheory/Regular/IsSMulRegular.lean

Chore(RingTheory/Regular): Simplify some namespaces in IsSMulRegular (#13582) …

Added isSMulRegular_algebraMap_iff View on Github →