Commit 2023-05-22 17:42 69632eec

View on Github →

feat: port LinearAlgebra.BilinearForm (#4202)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/BilinearForm.lean

added theorem BilinForm.IsAdjointPair.add

added theorem BilinForm.IsAdjointPair.comp

added theorem BilinForm.IsAdjointPair.eq

added theorem BilinForm.IsAdjointPair.mul

added theorem BilinForm.IsAdjointPair.smul

added theorem BilinForm.IsAdjointPair.sub

added def BilinForm.IsAdjointPair

added theorem BilinForm.IsAlt.isRefl

added theorem BilinForm.IsAlt.neg_eq

added theorem BilinForm.IsAlt.ortho_comm

added theorem BilinForm.IsAlt.self_eq_zero

added def BilinForm.IsAlt

added def BilinForm.IsOrtho

added def BilinForm.IsPairSelfAdjoint

added theorem BilinForm.IsRefl.eq_zero

added theorem BilinForm.IsRefl.ortho_comm

added def BilinForm.IsRefl

added def BilinForm.IsSelfAdjoint

added def BilinForm.IsSkewAdjoint

added theorem BilinForm.IsSymm.isRefl

added theorem BilinForm.IsSymm.ortho_comm

added def BilinForm.IsSymm

added theorem BilinForm.Nondegenerate.congr

added theorem BilinForm.Nondegenerate.ker_eq_bot

added theorem BilinForm.Nondegenerate.ne_zero

added def BilinForm.Nondegenerate

added theorem BilinForm.add_apply

added theorem BilinForm.add_left

added theorem BilinForm.add_right

added theorem BilinForm.apply_dualBasis_left

added theorem BilinForm.apply_dualBasis_right

added def BilinForm.coeFnAddMonoidHom

added theorem BilinForm.coeFn_congr

added theorem BilinForm.coeFn_mk

added theorem BilinForm.coe_add

added theorem BilinForm.coe_injective

added theorem BilinForm.coe_neg

added theorem BilinForm.coe_smul

added theorem BilinForm.coe_sub

added theorem BilinForm.coe_zero

added def BilinForm.comp

added def BilinForm.compLeft

added theorem BilinForm.compLeft_apply

added theorem BilinForm.compLeft_compRight

added theorem BilinForm.compLeft_id

added theorem BilinForm.compLeft_injective

added def BilinForm.compRight

added theorem BilinForm.compRight_apply

added theorem BilinForm.compRight_compLeft

added theorem BilinForm.compRight_id

added theorem BilinForm.comp_apply

added theorem BilinForm.comp_comp

added theorem BilinForm.comp_congr

added theorem BilinForm.comp_id_id

added theorem BilinForm.comp_id_left

added theorem BilinForm.comp_id_right

added theorem BilinForm.comp_inj

added theorem BilinForm.comp_symmCompOfNondegenerate_apply

added def BilinForm.congr

added theorem BilinForm.congr_apply

added theorem BilinForm.congr_comp

added theorem BilinForm.congr_congr

added theorem BilinForm.congr_fun

added theorem BilinForm.congr_refl

added theorem BilinForm.congr_symm

added theorem BilinForm.congr_trans

added theorem BilinForm.dualBasis_repr_apply

added theorem BilinForm.ext

added theorem BilinForm.ext_basis

added theorem BilinForm.ext_iff

added theorem BilinForm.finrank_add_finrank_orthogonal

added def BilinForm.flipHom

added def BilinForm.flipHomAux

added theorem BilinForm.flip_apply

added theorem BilinForm.flip_flip

added theorem BilinForm.flip_flip_aux

added theorem BilinForm.iIsOrtho.nondegenerate_iff_not_isOrtho_basis_self

added theorem BilinForm.iIsOrtho.not_isOrtho_basis_self_of_nondegenerate

added def BilinForm.iIsOrtho

added theorem BilinForm.iIsOrtho_def

added theorem BilinForm.isAdjointPairLeftAdjointOfNondegenerate

added theorem BilinForm.isAdjointPair_id

added theorem BilinForm.isAdjointPair_iff_compLeft_eq_compRight

added theorem BilinForm.isAdjointPair_iff_eq_of_nondegenerate

added theorem BilinForm.isAdjointPair_unique_of_nondegenerate

added theorem BilinForm.isAdjointPair_zero

added theorem BilinForm.isAlt_neg

added theorem BilinForm.isAlt_zero

added theorem BilinForm.isCompl_span_singleton_orthogonal

added theorem BilinForm.isOrtho_def

added theorem BilinForm.isOrtho_smul_left

added theorem BilinForm.isOrtho_smul_right

added theorem BilinForm.isOrtho_zero_left

added theorem BilinForm.isOrtho_zero_right

added def BilinForm.isPairSelfAdjointSubmodule

added theorem BilinForm.isPairSelfAdjoint_equiv

added theorem BilinForm.isRefl_neg

added theorem BilinForm.isRefl_zero

added theorem BilinForm.isSkewAdjoint_iff_neg_self_adjoint

added theorem BilinForm.isSymm_iff_flip'

added theorem BilinForm.isSymm_neg

added theorem BilinForm.isSymm_zero

added theorem BilinForm.le_orthogonal_orthogonal

added def BilinForm.linMulLin

added theorem BilinForm.linMulLin_apply

added theorem BilinForm.linMulLin_comp

added theorem BilinForm.linMulLin_compLeft

added theorem BilinForm.linMulLin_compRight

added theorem BilinForm.linearIndependent_of_iIsOrtho

added theorem BilinForm.mem_isPairSelfAdjointSubmodule

added theorem BilinForm.mem_orthogonal_iff

added theorem BilinForm.mem_selfAdjointSubmodule

added theorem BilinForm.mem_skewAdjointSubmodule

added theorem BilinForm.ne_zero_of_not_isOrtho_self

added theorem BilinForm.neg_apply

added theorem BilinForm.neg_left

added theorem BilinForm.neg_right

added theorem BilinForm.nondegenerateRestrictOfDisjointOrthogonal

added theorem BilinForm.nondegenerate_congr_iff

added theorem BilinForm.nondegenerate_iff_ker_eq_bot

added theorem BilinForm.not_nondegenerate_zero

added def BilinForm.orthogonal

added theorem BilinForm.orthogonal_le

added theorem BilinForm.orthogonal_span_singleton_eq_toLin_ker

added def BilinForm.restrict

added theorem BilinForm.restrictOrthogonalSpanSingletonNondegenerate

added theorem BilinForm.restrictSymm

added theorem BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal

added theorem BilinForm.restrict_nondegenerate_of_isCompl_orthogonal

added def BilinForm.selfAdjointSubmodule

added def BilinForm.skewAdjointSubmodule

added theorem BilinForm.smul_apply

added theorem BilinForm.smul_left

added theorem BilinForm.smul_right

added theorem BilinForm.span_singleton_inf_orthogonal_eq_bot

added theorem BilinForm.span_singleton_sup_orthogonal_eq_top

added theorem BilinForm.sub_apply

added theorem BilinForm.sub_left

added theorem BilinForm.sub_right

added theorem BilinForm.sum_left

added theorem BilinForm.sum_repr_mul_repr_mul

added theorem BilinForm.sum_right

added theorem BilinForm.symmCompOfNondegenerate_left_apply

added theorem BilinForm.toDual_def

added theorem BilinForm.toLin'Flip_apply

added theorem BilinForm.toLin'_apply

added def BilinForm.toLin

added def BilinForm.toLinHom

added def BilinForm.toLinHomAux₁

added def BilinForm.toLinHomAux₂

added def BilinForm.toLinHomFlip

added theorem BilinForm.toLin_apply

added theorem BilinForm.toLin_restrict_ker_eq_inf_orthogonal

added theorem BilinForm.toLin_restrict_range_dualCoannihilator_eq_orthogonal

added theorem BilinForm.toLin_symm

added theorem BilinForm.zero_apply

added theorem BilinForm.zero_left

added theorem BilinForm.zero_right

added structure BilinForm

added def LinearMap.compBilinForm

added def LinearMap.toBilin

added def LinearMap.toBilinAux

added theorem LinearMap.toBilinAux_eq

added theorem LinearMap.toBilin_symm