mathlib

678f62f0 - feat(data/polynomial): some lemmas about (nat)degree of bit0/1 in char_zero (#15726)