mathlib3

f94cd0f1 - feat(analysis/normed/normed_field): Pi types form a normed ring (#12912)