Commit 2024-07-08 11:32 ec3e05ab

View on Github →

chore(TwoSidedIdeal/Basic): apply forgotten review comments (#14462) After being delegated, I forgot to apply the suggestions from #13902 by @jcommelin ....

Estimated changes

Modified Mathlib/RingTheory/TwoSidedIdeal/Basic.lean

modified theorem TwoSidedIdeal.nsmul_mem

modified theorem TwoSidedIdeal.sub_mem

modified theorem TwoSidedIdeal.zsmul_mem