Commit 2021-12-21 12:42 a6b2f94a

View on Github →

refactor(linear_algebra/sesquilinear_form): Use similar definition as used in bilinear_map (#10443) Define sesquilinear forms as M →ₗ[R] M →ₛₗ[I] R.

Estimated changes

Modified src/analysis/inner_product_space/basic.lean

modified def sesq_form_of_inner

Modified src/linear_algebra/sesquilinear_form.lean

added theorem linear_map.is_alt.is_refl

added theorem linear_map.is_alt.neg

added theorem linear_map.is_alt.ortho_comm

added theorem linear_map.is_alt.self_eq_zero

added def linear_map.is_alt

added def linear_map.is_ortho

added theorem linear_map.is_ortho_def

added theorem linear_map.is_ortho_zero_left

added theorem linear_map.is_ortho_zero_right

added theorem linear_map.is_refl.eq_zero

added theorem linear_map.is_refl.ortho_comm

added def linear_map.is_refl

added theorem linear_map.is_symm.is_refl

added theorem linear_map.is_symm.ortho_comm

added def linear_map.is_symm

added theorem linear_map.ortho_smul_left

added theorem linear_map.ortho_smul_right

deleted theorem sesq_form.add_left

deleted def sesq_form.add_monoid_hom_right

deleted theorem sesq_form.add_right

deleted def sesq_form.comp

deleted theorem sesq_form.comp_apply

deleted theorem sesq_form.comp_comp

deleted theorem sesq_form.comp_injective

deleted def sesq_form.comp_left

deleted theorem sesq_form.comp_left_apply

deleted theorem sesq_form.comp_left_comp_right

deleted def sesq_form.comp_right

deleted theorem sesq_form.comp_right_apply

deleted theorem sesq_form.comp_right_comp_left

deleted theorem sesq_form.ext

deleted theorem sesq_form.is_alt.is_refl

deleted theorem sesq_form.is_alt.neg

deleted theorem sesq_form.is_alt.ortho_comm

deleted theorem sesq_form.is_alt.self_eq_zero

deleted def sesq_form.is_alt

deleted def sesq_form.is_ortho

deleted theorem sesq_form.is_refl.eq_zero

deleted theorem sesq_form.is_refl.ortho_comm

deleted def sesq_form.is_refl

deleted theorem sesq_form.is_symm.is_refl

deleted theorem sesq_form.is_symm.ortho_comm

deleted def sesq_form.is_symm

deleted def sesq_form.linear_map_left

deleted theorem sesq_form.neg_left

deleted theorem sesq_form.neg_right

deleted theorem sesq_form.ortho_smul_left

deleted theorem sesq_form.ortho_smul_right

deleted theorem sesq_form.ortho_zero

deleted theorem sesq_form.smul_left

deleted theorem sesq_form.smul_right

deleted theorem sesq_form.sub_left

deleted theorem sesq_form.sub_right

deleted theorem sesq_form.sum_left

deleted theorem sesq_form.sum_right

deleted theorem sesq_form.zero_left

deleted theorem sesq_form.zero_right

deleted structure sesq_form