mathlib

bc2f30ca - chore(algebra/order/ring): rename `.../nontrivial` to `.../char_zero` (#17562)