mathlib

d71cab9f - feat(analysis/seminorm): add composition with linear maps (#11477)

feat(analysis/seminorm): add composition with linear maps (#11477) This PR defines the composition of seminorms with linear maps and shows that composition is monotone and calculates the seminorm ball of the composition.