mathlib

d39c3a26 - feat(data/zsqrtd/basic): add some lemmas about norm (#7114)