mathlib

fae32b6e - refactor(analysis/normed_space/M_structure): generalize to arbitrary faithful actions (#14222)

refactor(analysis/normed_space/M_structure): generalize to arbitrary faithful actions (#14222) This follows up from a comment in review of #12173 The motivation here is to allow `X →L[𝕜] X`, `X →+ X`, and other weaker or stronger endomorphisms to also be used This also tides up a few proof names and some poorly-rendering LaTeX