Commit 2022-02-01 00:59 e37daad5

View on Github →

feat(linear_algebra/sesquilinear_form): Add orthogonality properties (#10992) Generalize lemmas about orthogonality from bilinear forms to sesquilinear forms.

Estimated changes

Modified src/linear_algebra/bilinear_map.lean

modified theorem linear_map.map_smul₂

Modified src/linear_algebra/sesquilinear_form.lean

added def linear_map.is_Ortho

added theorem linear_map.is_Ortho_def

modified def linear_map.is_alt

added theorem linear_map.is_compl_span_singleton_orthogonal

modified def linear_map.is_ortho

modified theorem linear_map.is_ortho_def

modified theorem linear_map.is_ortho_zero_left

modified theorem linear_map.is_ortho_zero_right

modified def linear_map.is_refl

modified theorem linear_map.is_symm.is_refl

modified theorem linear_map.is_symm.ortho_comm

added theorem linear_map.linear_independent_of_is_Ortho

modified theorem linear_map.ortho_smul_left

modified theorem linear_map.ortho_smul_right

added theorem linear_map.orthogonal_span_singleton_eq_to_lin_ker

added theorem linear_map.span_singleton_inf_orthogonal_eq_bot

added theorem linear_map.span_singleton_sup_orthogonal_eq_top

added theorem submodule.le_orthogonal_bilin_orthogonal_bilin

added theorem submodule.mem_orthogonal_bilin_iff

added def submodule.orthogonal_bilin

added theorem submodule.orthogonal_bilin_le