Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-10 20:28 60ccf8f7

View on Github →

feat(linear_algebra): add adjoint_pair from bilinear_form (#13203) Copying the definition and theorem about adjoint pairs from bilinear_form to sesquilinear_form. Defines the composition of two linear maps with a bilinear map to form a new bilinear map, which was missing from the bilinear_map API. We also use the new definition of adjoint pairs in analysis/inner_product_space/adjoint.

Estimated changes

Modified src/analysis/inner_product_space/adjoint.lean

deleted theorem continuous_linear_map.is_adjoint_pair

added theorem continuous_linear_map.is_adjoint_pair_inner

deleted theorem linear_map.is_adjoint_pair

added theorem linear_map.is_adjoint_pair_inner

Modified src/linear_algebra/bilinear_form.lean

added theorem bilin_form.comp_inj

deleted theorem bilin_form.comp_injective

Modified src/linear_algebra/bilinear_map.lean

added def linear_map.compl₁₂

added theorem linear_map.compl₁₂_apply

added theorem linear_map.compl₁₂_inj

Modified src/linear_algebra/sesquilinear_form.lean

added theorem linear_map.is_adjoint_pair.add

added theorem linear_map.is_adjoint_pair.comp

added theorem linear_map.is_adjoint_pair.mul

added theorem linear_map.is_adjoint_pair.smul

added theorem linear_map.is_adjoint_pair.sub

added def linear_map.is_adjoint_pair

added theorem linear_map.is_adjoint_pair_id

added theorem linear_map.is_adjoint_pair_iff_comp_eq_compl₂

added theorem linear_map.is_adjoint_pair_zero

added def linear_map.is_pair_self_adjoint

added theorem linear_map.is_pair_self_adjoint_equiv

added def linear_map.is_pair_self_adjoint_submodule

added def linear_map.is_skew_adjoint

added theorem linear_map.is_skew_adjoint_iff_neg_self_adjoint

added theorem linear_map.mem_is_pair_self_adjoint_submodule

added theorem linear_map.mem_self_adjoint_submodule

added theorem linear_map.mem_skew_adjoint_submodule

added def linear_map.self_adjoint_submodule

added def linear_map.skew_adjoint_submodule