Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-25 19:08 fae32b6e

View on Github →

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

Estimated changes

Modified src/analysis/normed_space/M_structure.lean

modified theorem is_Lprojection.Lcomplement

modified theorem is_Lprojection.Lcomplement_iff

modified theorem is_Lprojection.coe_bot

modified theorem is_Lprojection.coe_compl

modified theorem is_Lprojection.coe_inf

modified theorem is_Lprojection.coe_one

modified theorem is_Lprojection.coe_sdiff

modified theorem is_Lprojection.coe_sup

modified theorem is_Lprojection.coe_top

modified theorem is_Lprojection.coe_zero

modified theorem is_Lprojection.commute

added theorem is_Lprojection.compl_mul

deleted theorem is_Lprojection.compl_mul_left

deleted theorem is_Lprojection.compl_orthog

modified theorem is_Lprojection.distrib_lattice_lemma

modified theorem is_Lprojection.join

modified theorem is_Lprojection.le_def

modified theorem is_Lprojection.mul

added theorem is_Lprojection.mul_compl_self

modified structure is_Lprojection

modified structure is_Mprojection