Theorem Module.isTorsionBySet_annihilator

Modification history

2025-02-04 15:13

Mathlib/Algebra/Module/Torsion.lean

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

Modified Module.isTorsionBySet_annihilator View on Github →

2024-03-05 01:29

Mathlib/Algebra/Module/Torsion.lean

feat: sum and product of commuting semisimple endomorphisms (#10808) …

Added Module.isTorsionBySet_annihilator View on Github →