Theorem Ideal.jacobson_mul_mem_right

Modification history

2025-05-01 06:42
Mathlib/RingTheory/Jacobson/Ideal.lean
feat: preliminaries for Wedderburn–Artin (#24119)
Deleted Ideal.jacobson_mul_mem_rightView on Github →
2024-10-04 04:46
Mathlib/RingTheory/JacobsonIdeal.lean
feat(RingTheory): define two-sided Jacobson radical (#17341) …
Added Ideal.jacobson_mul_mem_rightView on Github →