feat(analysis/inner_product_space/finite_dimensional): some lemmas on finite dimensional inner product spaces #18041
Conversation
…le for finite dimensional inner product space
themathqueen
added
WIP
|
These proofs look substantially longer than I would expect. I don't have time to look at them today, unfortunately. Maybe @ADedecker has some time? Edit: I hadn't seen that Anatole already self-assigned. Even better! |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
eric-wieser
removed
the
awaiting-review
themathqueen
added
awaiting-review
| variables [ring R] [add_comm_group M] [topological_add_group M] [module R M] | ||
|
|
||
| /-- Given an invertible operator, multiplying it by its inverse gives the identity. -/ | ||
| lemma inv_mul_self (T : M →L[R] M) [invertible T] : T.inverse * T = 1 := |
There was a problem hiding this comment.
Usually we only use invertible if you use \frac1 (aka inv_of) in the statement. Since you don't, can you use is_unit T instead?
There was a problem hiding this comment.
Wouldn't it be easier to use \frac1 instead of inv_of everywhere?
There was a problem hiding this comment.
inv_of is to \frac1 as mul is to *. We use one in lemma names, but the other is the operator.
| lemma submodule.commutes_with_linear_proj_iff_linear_proj_eq [invertible T] : | ||
| commute (U.subtype.comp eᵤ) T ↔ | ||
| (⅟ T).comp ((U.subtype.comp eᵤ).comp T) = U.subtype.comp eᵤ := |
There was a problem hiding this comment.
My feeling would be to avoid all the invertible stuff by assuming T to be linear_equiv here, but maybe that will backfire later in applications. @eric-wieser what do you think ?
|
@ADedecker @eric-wieser should I make a new PR only containing the |
|
Sorry for the slow response. Yes, I think that would be nice, because this PR is getting quite large (for good reasons!) |
…ommunity/mathlib into finite_dimensional_inner_product_spaces
themathqueen
added
the
blocked-by-other-PR
mathlib-dependent-issues-bot
removed
the
blocked-by-other-PR
themathqueen
changed the title
Vierkantor
added
the
blocked-by-other-PR
eric-wieser
added
the
not-too-late
Created new file to start proving results in finite-dimensional inner product spaces.
orthogonal_projectionusinglinear_proj_of_is_compl#18243