Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-04 13:36 b3b7fe67

View on Github →

chore(algebra/module): generalize char_zero.of_algebra to char_zero.of_module (#10609)

Estimated changes

deleted theorem char_zero.of_algebra
added theorem char_zero.of_module