Commit 2023-12-08 09:00 41bbd194

View on Github →

chore: Split LinearAlgebra.BilinearForm. (#8879) Also renamed BilinearForm.restrictSymm to BilinearForm.IsSymm.restrict.

Estimated changes

deleted theorem BilinForm.IsAlt.isRefl
deleted theorem BilinForm.IsAlt.neg_eq
deleted def BilinForm.IsAlt
deleted def BilinForm.IsOrtho
deleted theorem BilinForm.IsRefl.eq_zero
deleted def BilinForm.IsRefl
deleted theorem BilinForm.IsSymm.isRefl
deleted def BilinForm.IsSymm
deleted theorem BilinForm.add_apply
deleted theorem BilinForm.add_left
deleted theorem BilinForm.add_right
deleted theorem BilinForm.coeFn_congr
deleted theorem BilinForm.coeFn_mk
deleted theorem BilinForm.coe_add
deleted theorem BilinForm.coe_injective
deleted theorem BilinForm.coe_neg
deleted theorem BilinForm.coe_smul
deleted theorem BilinForm.coe_sub
deleted theorem BilinForm.coe_zero
deleted def BilinForm.comp
deleted def BilinForm.compLeft
deleted theorem BilinForm.compLeft_apply
deleted theorem BilinForm.compLeft_id
deleted def BilinForm.compRight
deleted theorem BilinForm.compRight_apply
deleted theorem BilinForm.compRight_id
deleted theorem BilinForm.comp_apply
deleted theorem BilinForm.comp_comp
deleted theorem BilinForm.comp_congr
deleted theorem BilinForm.comp_id_id
deleted theorem BilinForm.comp_id_left
deleted theorem BilinForm.comp_id_right
deleted theorem BilinForm.comp_inj
deleted def BilinForm.congr
deleted theorem BilinForm.congr_apply
deleted theorem BilinForm.congr_comp
deleted theorem BilinForm.congr_congr
deleted theorem BilinForm.congr_fun
deleted theorem BilinForm.congr_refl
deleted theorem BilinForm.congr_symm
deleted theorem BilinForm.congr_trans
deleted theorem BilinForm.ext
deleted theorem BilinForm.ext_basis
deleted theorem BilinForm.ext_iff
deleted def BilinForm.flipHom
deleted theorem BilinForm.flip_apply
deleted theorem BilinForm.flip_flip
deleted theorem BilinForm.flip_flip_aux
deleted def BilinForm.iIsOrtho
deleted theorem BilinForm.iIsOrtho_def
deleted theorem BilinForm.isAlt_neg
deleted theorem BilinForm.isAlt_zero
deleted theorem BilinForm.isOrtho_def
deleted theorem BilinForm.isRefl_neg
deleted theorem BilinForm.isRefl_zero
deleted theorem BilinForm.isSymm_iff_flip
deleted theorem BilinForm.isSymm_neg
deleted theorem BilinForm.isSymm_zero
deleted def BilinForm.linMulLin
deleted theorem BilinForm.linMulLin_apply
deleted theorem BilinForm.linMulLin_comp
deleted theorem BilinForm.neg_apply
deleted theorem BilinForm.neg_left
deleted theorem BilinForm.neg_right
deleted theorem BilinForm.orthogonal_le
deleted def BilinForm.restrict
deleted theorem BilinForm.restrictSymm
deleted theorem BilinForm.smul_apply
deleted theorem BilinForm.smul_left
deleted theorem BilinForm.smul_right
deleted theorem BilinForm.sub_apply
deleted theorem BilinForm.sub_left
deleted theorem BilinForm.sub_right
deleted theorem BilinForm.sum_apply
deleted theorem BilinForm.sum_left
deleted theorem BilinForm.sum_right
deleted theorem BilinForm.toDual_def
deleted theorem BilinForm.toLin'_apply
deleted def BilinForm.toLin
deleted def BilinForm.toLinHom
deleted theorem BilinForm.toLin_apply
deleted theorem BilinForm.toLin_symm
deleted theorem BilinForm.zero_apply
deleted theorem BilinForm.zero_left
deleted theorem BilinForm.zero_right
deleted structure BilinForm
deleted def LinearMap.toBilin
deleted theorem LinearMap.toBilinAux_eq
deleted theorem LinearMap.toBilin_apply
deleted theorem LinearMap.toBilin_symm
added theorem BilinForm.add_apply
added theorem BilinForm.add_left
added theorem BilinForm.add_right
added theorem BilinForm.coeFn_congr
added theorem BilinForm.coeFn_mk
added theorem BilinForm.coe_add
added theorem BilinForm.coe_neg
added theorem BilinForm.coe_smul
added theorem BilinForm.coe_sub
added theorem BilinForm.coe_zero
added theorem BilinForm.congr_fun
added theorem BilinForm.ext
added theorem BilinForm.ext_iff
added theorem BilinForm.flip_apply
added theorem BilinForm.flip_flip
added theorem BilinForm.neg_apply
added theorem BilinForm.neg_left
added theorem BilinForm.neg_right
added theorem BilinForm.smul_apply
added theorem BilinForm.smul_left
added theorem BilinForm.smul_right
added theorem BilinForm.sub_apply
added theorem BilinForm.sub_left
added theorem BilinForm.sub_right
added theorem BilinForm.zero_apply
added theorem BilinForm.zero_left
added theorem BilinForm.zero_right
added structure BilinForm
added def BilinForm.comp
added theorem BilinForm.compLeft_id
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_inj
added def BilinForm.congr
added theorem BilinForm.congr_apply
added theorem BilinForm.congr_comp
added theorem BilinForm.congr_congr
added theorem BilinForm.congr_refl
added theorem BilinForm.congr_symm
added theorem BilinForm.congr_trans
added theorem BilinForm.ext_basis
added theorem BilinForm.sum_apply
added theorem BilinForm.sum_left
added theorem BilinForm.sum_right
added theorem BilinForm.toLin'_apply
added def BilinForm.toLin
added theorem BilinForm.toLin_apply
added theorem BilinForm.toLin_symm
added theorem LinearMap.toBilin_symm
added theorem BilinForm.iIsOrtho_def
added theorem BilinForm.isOrtho_def
added theorem BilinForm.IsAlt.isRefl
added theorem BilinForm.IsAlt.neg_eq
added def BilinForm.IsAlt
added def BilinForm.IsRefl
added def BilinForm.IsSymm
added theorem BilinForm.isAlt_neg
added theorem BilinForm.isAlt_zero
added theorem BilinForm.isRefl_neg
added theorem BilinForm.isRefl_zero
added theorem BilinForm.isSymm_neg
added theorem BilinForm.isSymm_zero
added theorem BilinForm.toDual_def