mathlib3

fe435de8 - feat(algebra/algebra/basic,analysis/normed_space/basic): The zero ring is a (normed) algebra (#13618)

feat(algebra/algebra/basic,analysis/normed_space/basic): The zero ring is a (normed) algebra (#13618) This instance probably isn't very useful, but it's nice to have in the docs as an example of what `normed_algebra` permits.