Commit 2023-08-20 16:14 a1bb5932

View on Github →

feat(Mathlib/Algebra/CharP/Basic): add ringChar_zero_iff_CharZero (#6572) Zulip discussion

Estimated changes