Def Module.IsTorsionBySet.semilinearMap

Modification history

2025-02-04 15:13

Mathlib/Algebra/Module/Torsion.lean

refactor: introduce `Ideal.IsTwoSided` class for quotients of noncommutative rings (#17930)

Added Module.IsTorsionBySet.semilinearMap View on Github →