Commit 2023-06-05 12:54 648a40a2

View on Github →

feat: port LinearAlgebra.QuadraticForm.Basic (#4432)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Nat/Cast/Basic.lean

added theorem Commute.ofNat_left

added theorem Commute.ofNat_right

Created Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

added theorem BilinForm.exists_bilinForm_self_ne_zero

added theorem BilinForm.exists_orthogonal_basis

added theorem BilinForm.nondegenerate_of_anisotropic

added theorem BilinForm.polar_to_quadratic_form

added def BilinForm.toQuadraticForm

added def BilinForm.toQuadraticFormAddMonoidHom

added theorem BilinForm.toQuadraticForm_add

added theorem BilinForm.toQuadraticForm_apply

added theorem BilinForm.toQuadraticForm_eq_zero

added theorem BilinForm.toQuadraticForm_list_sum

added theorem BilinForm.toQuadraticForm_multiset_sum

added theorem BilinForm.toQuadraticForm_neg

added theorem BilinForm.toQuadraticForm_smul

added theorem BilinForm.toQuadraticForm_sub

added theorem BilinForm.toQuadraticForm_sum

added theorem BilinForm.toQuadraticForm_zero

added def LinearMap.compQuadraticForm

added def Matrix.toQuadraticForm'

added theorem QuadraticForm.Anisotropic.eq_zero_iff

added def QuadraticForm.Anisotropic

added theorem QuadraticForm.PosDef.add

added theorem QuadraticForm.PosDef.anisotropic

added theorem QuadraticForm.PosDef.nonneg

added theorem QuadraticForm.PosDef.smul

added def QuadraticForm.PosDef

added theorem QuadraticForm.add_apply

added theorem QuadraticForm.add_linMulLin

added def QuadraticForm.associatedHom

added theorem QuadraticForm.associated_apply

added theorem QuadraticForm.associated_comp

added theorem QuadraticForm.associated_eq_self_apply

added theorem QuadraticForm.associated_isSymm

added theorem QuadraticForm.associated_left_inverse

added theorem QuadraticForm.associated_linMulLin

added theorem QuadraticForm.associated_rightInverse

added theorem QuadraticForm.associated_toQuadraticForm

added theorem QuadraticForm.basisRepr_apply

added theorem QuadraticForm.basisRepr_eq_of_iIsOrtho

added theorem QuadraticForm.choose_exists_companion

added def QuadraticForm.coeFnAddMonoidHom

added theorem QuadraticForm.coeFn_add

added theorem QuadraticForm.coeFn_neg

added theorem QuadraticForm.coeFn_smul

added theorem QuadraticForm.coeFn_sub

added theorem QuadraticForm.coeFn_sum

added theorem QuadraticForm.coeFn_zero

added theorem QuadraticForm.coe_copy

added def QuadraticForm.comp

added theorem QuadraticForm.comp_apply

added theorem QuadraticForm.congr_fun

added theorem QuadraticForm.copy_eq

added def QuadraticForm.discr

added theorem QuadraticForm.discr_comp

added theorem QuadraticForm.discr_smul

added def QuadraticForm.evalAddMonoidHom

added theorem QuadraticForm.exists_companion

added theorem QuadraticForm.exists_quadraticForm_ne_zero

added theorem QuadraticForm.ext

added theorem QuadraticForm.ext_iff

added theorem QuadraticForm.isSymm_toMatrix'

added def QuadraticForm.linMulLin

added theorem QuadraticForm.linMulLinSelfPosDef

added theorem QuadraticForm.linMulLin_add

added theorem QuadraticForm.linMulLin_apply

added theorem QuadraticForm.linMulLin_comp

added theorem QuadraticForm.map_add_add_add_map

added theorem QuadraticForm.map_add_self

added theorem QuadraticForm.map_neg

added theorem QuadraticForm.map_smul

added theorem QuadraticForm.map_smul_of_tower

added theorem QuadraticForm.map_sub

added theorem QuadraticForm.map_zero

added theorem QuadraticForm.neg_apply

added theorem QuadraticForm.nondegenerate_of_anisotropic

added theorem QuadraticForm.not_anisotropic_iff_exists

added def QuadraticForm.ofPolar

added def QuadraticForm.polar

added def QuadraticForm.polarBilin

added theorem QuadraticForm.polar_add

added theorem QuadraticForm.polar_add_left

added theorem QuadraticForm.polar_add_left_iff

added theorem QuadraticForm.polar_add_right

added theorem QuadraticForm.polar_comm

added theorem QuadraticForm.polar_comp

added theorem QuadraticForm.polar_neg

added theorem QuadraticForm.polar_neg_left

added theorem QuadraticForm.polar_neg_right

added theorem QuadraticForm.polar_self

added theorem QuadraticForm.polar_smul

added theorem QuadraticForm.polar_smul_left

added theorem QuadraticForm.polar_smul_left_of_tower

added theorem QuadraticForm.polar_smul_right

added theorem QuadraticForm.polar_smul_right_of_tower

added theorem QuadraticForm.polar_sub_left

added theorem QuadraticForm.polar_sub_right

added theorem QuadraticForm.polar_zero_left

added theorem QuadraticForm.polar_zero_right

added theorem QuadraticForm.posDefOfNonneg

added theorem QuadraticForm.posDef_iff_nonneg

added def QuadraticForm.proj

added theorem QuadraticForm.proj_apply

added theorem QuadraticForm.smul_apply

added def QuadraticForm.sq

added theorem QuadraticForm.sub_apply

added theorem QuadraticForm.sum_apply

added theorem QuadraticForm.toFun_eq_coe

added def QuadraticForm.toMatrix'

added theorem QuadraticForm.toMatrix'_comp

added theorem QuadraticForm.toMatrix'_smul

added theorem QuadraticForm.toQuadraticForm_associated

added def QuadraticForm.weightedSumSquares

added theorem QuadraticForm.weightedSumSquares_apply

added theorem QuadraticForm.zero_apply

added structure QuadraticForm