Basic

📁 Source: Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

Statistics

Metric	Count
Definitions congrQuadraticMap, toQuadraticMap, toQuadraticMapAddMonoidHom, toQuadraticMapLinearMap, compQuadraticMap, compQuadraticMap', toQuadraticMap', Anisotropic, IsOrtho, associated, associated', associatedHom, basisRepr, coeFnAddMonoidHom, comp, copy, discr, evalAddMonoidHom, instAdd, instAddCommGroup, instAddCommMonoid, instDistribMulActionOfSMulCommClass, instFunLike, instInhabited, instInvertibleEndOfNat, instModuleOfSMulCommClass, instNeg, instSMul, instSub, instZero, linMulLin, ofPolar, polar, polarBilin, polarSym2, proj, restrictScalars, sq, toFun, toMatrix', weightedSumSquares	41
Theorems congrQuadraticMap_apply, congrQuadraticMap_refl, congrQuadraticMap_symm, congrQuadraticMap_symm_apply, exists_bilinForm_self_ne_zero, exists_orthogonal_basis, separatingLeft_of_anisotropic, toQuadraticMap_isOrtho, polarBilin_toQuadraticMap, polar_toQuadraticMap, toQuadraticMapAddMonoidHom_apply, toQuadraticMapLinearMap_apply, toQuadraticMap_add, toQuadraticMap_apply, toQuadraticMap_comp_same, toQuadraticMap_eq_zero, toQuadraticMap_list_sum, toQuadraticMap_multiset_sum, toQuadraticMap_neg, toQuadraticMap_smul, toQuadraticMap_sub, toQuadraticMap_sum, toQuadraticMap_zero, compQuadraticMap'_apply, compQuadraticMap_apply, compQuadraticMap_polar, compQuadraticMap_polarBilin, associated_isSymm, eq_zero_iff, all, polar_eq_zero, zero_left, zero_right, add, anisotropic, le_zero_iff, nonneg, smul, add_apply, add_linMulLin, associated_apply, associated_comp, associated_eq_self_apply, associated_flip, associated_isOrtho, associated_isSymm, associated_left_inverse, associated_left_inverse', associated_linMulLin, associated_rightInverse, associated_sq, associated_toQuadraticMap, basisRepr_apply, basisRepr_eq_of_iIsOrtho, canLift, canLift', choose_exists_companion, coeFnAddMonoidHom_apply, coeFn_add, coeFn_neg, coeFn_smul, coeFn_sub, coeFn_sum, coeFn_zero, coe_associatedHom, coe_copy, coe_mk, comp_apply, congr_fun, copy_eq, discr_comp, discr_smul, evalAddMonoidHom_apply, exists_companion, exists_companion', exists_quadraticMap_ne_zero, ext, ext_iff, half_moduleEnd_apply_eq_half_smul, instIsScalarTower, instSMulCommClass, isOrtho_comm, isOrtho_def, isOrtho_polarBilin, isSymm_toMatrix', linMulLinSelfPosDef, linMulLin_add, linMulLin_apply, linMulLin_comp, map_add, map_add_add_add_map, map_add_self, map_neg, map_smul, map_smul_of_tower, map_sub, map_sum, map_sum', map_zero, ne_zero_of_not_isOrtho_self, neg_apply, not_anisotropic_iff_exists, ofPolar_apply, polarBilin_apply_apply, polarBilin_comp, polarBilin_injective, polarSym2_map_smul, polarSym2_sym2Mk, polar_add, polar_add_left, polar_add_left_iff, polar_add_right, polar_comm, polar_comp, polar_neg, polar_neg_left, polar_neg_right, polar_self, polar_smul, polar_smul_left, polar_smul_left_of_tower, polar_smul_right, polar_smul_right_of_tower, polar_sub_left, polar_sub_right, polar_zero_left, polar_zero_right, posDef_iff_nonneg, posDef_of_nonneg, proj_apply, restrictScalars_apply, separatingLeft_of_anisotropic, smul_apply, sq_apply, sub_apply, sum_apply, toFun_eq_coe, toFun_smul, toMatrix'_comp, toMatrix'_smul, toQuadraticMap_associated, toQuadraticMap_polarBilin, two_nsmul_associated, weightedSumSquares_apply, zeroHomClass, zero_apply	146
Total	187

LinearEquiv

Definitions

Name	Category	Theorems
congrQuadraticMap 📖	CompOp	4 math math: congrQuadraticMap_symm, congrQuadraticMap_refl, congrQuadraticMap_symm_apply, congrQuadraticMap_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congrQuadraticMap_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids QuadraticMap QuadraticMap.instAddCommMonoid QuadraticMap.instModuleOfSMulCommClass smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike instEquivLike congrQuadraticMap LinearMap.compQuadraticMap toLinearMap	—	RingHomInvPair.ids smulCommClass_self
congrQuadraticMap_refl 📖	mathematical	—	congrQuadraticMap refl CommSemiring.toSemiring QuadraticMap QuadraticMap.instAddCommMonoid QuadraticMap.instModuleOfSMulCommClass smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	RingHomInvPair.ids smulCommClass_self
congrQuadraticMap_symm 📖	mathematical	—	symm QuadraticMap CommSemiring.toSemiring QuadraticMap.instAddCommMonoid QuadraticMap.instModuleOfSMulCommClass smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids congrQuadraticMap	—	RingHomInvPair.ids smulCommClass_self
congrQuadraticMap_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids QuadraticMap QuadraticMap.instAddCommMonoid QuadraticMap.instModuleOfSMulCommClass smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike instEquivLike symm congrQuadraticMap LinearMap.compQuadraticMap toLinearMap	—	RingHomInvPair.ids smulCommClass_self

LinearMap

Definitions

Name	Category	Theorems
compQuadraticMap 📖	CompOp	3 math math: compQuadraticMap_apply, LinearEquiv.congrQuadraticMap_symm_apply, LinearEquiv.congrQuadraticMap_apply
compQuadraticMap' 📖	CompOp	3 math math: compQuadraticMap_polar, compQuadraticMap'_apply, compQuadraticMap_polarBilin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compQuadraticMap'_apply 📖	mathematical	—	DFunLike.coe QuadraticMap QuadraticMap.instFunLike compQuadraticMap' LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring instFunLike	—	—
compQuadraticMap_apply 📖	mathematical	—	DFunLike.coe QuadraticMap QuadraticMap.instFunLike compQuadraticMap LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring instFunLike	—	—
compQuadraticMap_polar 📖	mathematical	—	QuadraticMap.polar DFunLike.coe QuadraticMap AddCommGroup.toAddCommMonoid QuadraticMap.instFunLike compQuadraticMap' CommRing.toCommSemiring LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring instFunLike	—	map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass
compQuadraticMap_polarBilin 📖	mathematical	—	QuadraticMap.polarBilin compQuadraticMap' CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction compr₂ Semiring.toModule smulCommClass_self CommRing.toCommMonoid CommMonoid.toMonoid Ring.toSemiring CommRing.toRing	—	ext IsScalarTower.left smulCommClass_self QuadraticMap.polarBilin_apply_apply compr₂_apply compQuadraticMap_polar

LinearMap.BilinForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_bilinForm_self_ne_zero 📖	mathematical	LinearMap.IsSymm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	LinearMap.IsOrtho NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass IsScalarTower.right IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass CanLift.prf QuadraticMap.canLift QuadraticMap.exists_quadraticMap_ne_zero QuadraticMap.associated_eq_self_apply
exists_orthogonal_basis 📖	mathematical	LinearMap.IsSymm Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	LinearMap.IsOrthoᵢ Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule DFunLike.coe Module.Basis Module.Basis.instFunLike	—	Nat.instAtLeastTwoHAddOfNat Fin.isEmpty' map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass eq_or_ne IsNoetherianRing.strongRankCondition EuclideanDomain.toNontrivial PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain Module.Free.of_divisionRing exists_bilinForm_self_ne_zero Algebra.to_smulCommClass FiniteDimensional.finiteDimensional_submodule LinearMap.IsSymm.domRestrict finrank_span_singleton ne_zero_of_map Submodule.finrank_add_eq_of_isCompl IsCompl.symm LinearMap.isCompl_span_singleton_orthogonal IsCompl.disjoint Submodule.disjoint_def Submodule.smul_mem Submodule.mem_span_singleton_self Submodule.neg_mem_iff add_eq_zero_iff_neg_eq smul_eq_zero instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero Submodule.mem_span_singleton LinearMap.IsOrtho.eq_1 map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.smul_apply map_add SemilinearMapClass.toAddHomClass smul_eq_mul div_mul_cancel₀ add_neg_cancel MulZeroClass.mul_zero Module.Basis.coe_mkFinCons Fin.cons_zero Fin.cons_succ LinearMap.IsSymm.eq Subtype.prop
separatingLeft_of_anisotropic 📖	mathematical	QuadraticMap.Anisotropic NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule LinearMap.BilinMap.toQuadraticMap	LinearMap.SeparatingLeft RingHom.id	—	—
toQuadraticMap_isOrtho 📖	mathematical	LinearMap.IsSymm RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	QuadraticMap.IsOrtho NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.BilinMap.toQuadraticMap LinearMap.IsOrtho	—	smulCommClass_self map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass add_comm add_add_add_comm add_eq_left AddLeftCancelSemigroup.toIsLeftCancelAdd IsCancelAdd.toIsLeftCancelAdd IsCancelAdd.toIsRightCancelAdd Algebra.to_smulCommClass LinearMap.IsSymm.eq RingHom.id_apply add_self_eq_zero

LinearMap.BilinMap

Definitions

Name	Category	Theorems
toQuadraticMap 📖	CompOp	31 math math: polar_toQuadraticMap, toQuadraticMap_add, toQuadraticMapAddMonoidHom_apply, RootPairing.rootForm_anisotropic, toQuadraticMap_zero, QuadraticMap.associated_rightInverse, CliffordAlgebra.changeForm.zero_proof, toQuadraticMap_eq_zero, QuadraticMap.toQuadraticMap_associated, QuadraticMap.associated_left_inverse, RootSystem.rootForm_anisotropic, LinearMap.BilinForm.toQuadraticMap_isOrtho, QuadraticMap.associated_toQuadraticMap, QuadraticMap.associated_left_inverse', QuadraticMap.toQuadraticMap_polarBilin, toQuadraticMap_smul, toQuadraticMapLinearMap_apply, toQuadraticMap_surjective, toQuadraticMap_list_sum, toQuadraticMap_multiset_sum, QuadraticMap.toQuadraticMap_toBilin, toQuadraticMap_sum, CliffordAlgebra.changeForm.associated_neg_proof, RootPairing.posRootForm_posForm_anisotropic, toQuadraticMap_apply, polarBilin_toQuadraticMap, RootPairing.posRootForm_rootFormIn_posDef, toQuadraticMap_neg, toQuadraticMap_comp_same, LinearMap.dualProd.toQuadraticForm, toQuadraticMap_sub
toQuadraticMapAddMonoidHom 📖	CompOp	1 math math: toQuadraticMapAddMonoidHom_apply
toQuadraticMapLinearMap 📖	CompOp	1 math math: toQuadraticMapLinearMap_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
polarBilin_toQuadraticMap 📖	mathematical	—	QuadraticMap.polarBilin toQuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.BilinMap LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction LinearMap.instAdd LinearMap.flip	—	LinearMap.ext₂ SMulCommClass.symm polar_toQuadraticMap
polar_toQuadraticMap 📖	mathematical	—	QuadraticMap.polar DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid QuadraticMap.instFunLike toQuadraticMap AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.BilinMap LinearMap.addCommMonoid LinearMap.module	—	map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass add_assoc add_comm add_sub_cancel_left sub_eq_add_neg add_neg_cancel_left
toQuadraticMapAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom LinearMap.BilinMap QuadraticMap AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearMap.addCommMonoid LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.module QuadraticMap.instAddCommMonoid AddMonoidHom.instFunLike toQuadraticMapAddMonoidHom toQuadraticMap	—	—
toQuadraticMapLinearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.BilinMap QuadraticMap LinearMap.addCommMonoid CommSemiring.toSemiring LinearMap.module QuadraticMap.instAddCommMonoid LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction QuadraticMap.instModuleOfSMulCommClass LinearMap.instFunLike toQuadraticMapLinearMap toQuadraticMap	—	LinearMap.instSMulCommClass
toQuadraticMap_add 📖	mathematical	—	toQuadraticMap LinearMap.BilinMap LinearMap.instAdd LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module QuadraticMap QuadraticMap.instAdd	—	—
toQuadraticMap_apply 📖	mathematical	—	DFunLike.coe QuadraticMap QuadraticMap.instFunLike toQuadraticMap LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.BilinMap LinearMap.addCommMonoid LinearMap.module	—	—
toQuadraticMap_comp_same 📖	mathematical	—	toQuadraticMap LinearMap.compl₁₂ CommSemiring.toSemiring QuadraticMap.comp	—	—
toQuadraticMap_eq_zero 📖	mathematical	—	toQuadraticMap QuadraticMap QuadraticMap.instZero LinearMap.IsAlt RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	QuadraticMap.ext_iff
toQuadraticMap_list_sum 📖	mathematical	—	toQuadraticMap LinearMap.BilinMap LinearMap.instAdd LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module LinearMap.instZero QuadraticMap QuadraticMap.instAdd QuadraticMap.instZero	—	map_list_sum AddMonoidHom.instAddMonoidHomClass
toQuadraticMap_multiset_sum 📖	mathematical	—	toQuadraticMap Multiset.sum LinearMap.BilinMap LinearMap.addCommMonoid LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.module QuadraticMap QuadraticMap.instAddCommMonoid Multiset.map	—	map_multiset_sum AddMonoidHom.instAddMonoidHomClass
toQuadraticMap_neg 📖	mathematical	—	toQuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.BilinMap LinearMap.instNeg LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommGroup LinearMap.module QuadraticMap QuadraticMap.instNeg	—	—
toQuadraticMap_smul 📖	mathematical	—	toQuadraticMap LinearMap.BilinMap LinearMap.instSMul LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid LinearMap.instDistribMulAction LinearMap.instSMulCommClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction QuadraticMap QuadraticMap.instSMul	—	LinearMap.instSMulCommClass
toQuadraticMap_sub 📖	mathematical	—	toQuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.BilinMap LinearMap.instSub LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommGroup LinearMap.module QuadraticMap QuadraticMap.instSub	—	—
toQuadraticMap_sum 📖	mathematical	—	toQuadraticMap Finset.sum LinearMap.BilinMap LinearMap.addCommMonoid LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.module QuadraticMap QuadraticMap.instAddCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass
toQuadraticMap_zero 📖	mathematical	—	toQuadraticMap LinearMap.BilinMap LinearMap.instZero LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module QuadraticMap QuadraticMap.instZero	—	—

Matrix

Definitions

Name	Category	Theorems
toQuadraticMap' 📖	CompOp	1 math math: PosDef.toQuadraticForm'

QuadraticForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associated_isSymm 📖	mathematical	—	LinearMap.IsSymm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe LinearMap QuadraticMap Ring.toAddCommGroup CommRing.toRing Semiring.toModule LinearMap.BilinMap QuadraticMap.instAddCommMonoid LinearMap.addCommMonoid LinearMap.module QuadraticMap.instModuleOfSMulCommClass Algebra.toModule IsScalarTower.to_smulCommClass IsScalarTower.right IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike QuadraticMap.associatedHom QuadraticMap.instInvertibleEndOfNat	—	Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass IsScalarTower.right IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass QuadraticMap.associated_isSymm

QuadraticMap

Definitions

Name	Category	Theorems
Anisotropic 📖	MathDef	6 math math: not_anisotropic_iff_exists, RootPairing.rootForm_anisotropic, RootSystem.rootForm_anisotropic, PosDef.anisotropic, RootPairing.posRootForm_posForm_anisotropic, posDef_iff_nonneg
IsOrtho 📖	MathDef	12 math math: isOrtho_comm, isOrtho_inl_inl_iff, IsOrtho.all, isOrtho_def, LinearMap.BilinForm.toQuadraticMap_isOrtho, isOrtho_polarBilin, IsOrtho.zero_left, IsOrtho.inr_inl, isOrtho_inr_inr_iff, associated_isOrtho, IsOrtho.zero_right, IsOrtho.inl_inr
associated 📖	CompOp	11 math math: associated_prod, associated_tmul, QuadraticForm.toDualProd_apply, coe_associatedHom, associated_linMulLin, associated_sq, associated_isOrtho, Ring.associated_pi, CliffordAlgebra.changeForm.associated_neg_proof, QuadraticForm.associated_tmul, QuadraticForm.associated_baseChange
associated' 📖	CompOp	1 math math: separatingLeft_of_anisotropic
associatedHom 📖	CompOp	15 math math: canLift, associated_eq_self_apply, associated_rightInverse, associated_apply, toQuadraticMap_associated, associated_left_inverse, associated_toQuadraticMap, two_nsmul_associated, associated_left_inverse', canLift', coe_associatedHom, QuadraticForm.associated_isSymm, associated_comp, associated_flip, associated_isSymm
basisRepr 📖	CompOp	2 math math: basisRepr_eq_of_iIsOrtho, basisRepr_apply
coeFnAddMonoidHom 📖	CompOp	1 math math: coeFnAddMonoidHom_apply
comp 📖	CompOp	12 math math: toMatrix'_comp, QuadraticForm.tmul_comp_tensorComm, comp_apply, QuadraticForm.comp_tensorLId_eq, discr_comp, QuadraticForm.tmul_comp_tensorMap, QuadraticForm.comp_tensorRId_eq, associated_comp, QuadraticForm.tmul_comp_tensorAssoc, polarBilin_comp, linMulLin_comp, LinearMap.BilinMap.toQuadraticMap_comp_same
copy 📖	CompOp	2 math math: coe_copy, copy_eq
discr 📖	CompOp	2 math math: discr_smul, discr_comp
evalAddMonoidHom 📖	CompOp	1 math math: evalAddMonoidHom_apply
instAdd 📖	CompOp	8 math math: LinearMap.BilinMap.toQuadraticMap_add, add_linMulLin, add_toBilin, coeFn_add, LinearMap.BilinMap.toQuadraticMap_list_sum, PosDef.add, linMulLin_add, add_apply
instAddCommGroup 📖	CompOp	2 math math: toQuadraticMap_polarBilin, separatingLeft_of_anisotropic
instAddCommMonoid 📖	CompOp	42 math math: canLift, LinearEquiv.congrQuadraticMap_symm, LinearMap.BilinMap.toQuadraticMapAddMonoidHom_apply, toBilinHom_apply, associated_eq_self_apply, associated_rightInverse, sum_apply, LinearEquiv.congrQuadraticMap_refl, associated_prod, associated_apply, toQuadraticMap_associated, associated_left_inverse, evalAddMonoidHom_apply, associated_tmul, associated_toQuadraticMap, two_nsmul_associated, associated_left_inverse', coeFnAddMonoidHom_apply, LinearMap.BilinMap.toQuadraticMapLinearMap_apply, QuadraticForm.tensorDistrib_tmul, QuadraticForm.toDualProd_apply, canLift', LinearMap.BilinMap.toQuadraticMap_multiset_sum, coe_associatedHom, LinearEquiv.congrQuadraticMap_symm_apply, associated_linMulLin, QuadraticForm.associated_isSymm, LinearMap.BilinMap.toQuadraticMap_sum, associated_sq, associated_comp, associated_isOrtho, Ring.associated_pi, coeFn_sum, CliffordAlgebra.changeForm.associated_neg_proof, separatingLeft_of_anisotropic, LinearEquiv.congrQuadraticMap_apply, QuadraticForm.associated_tmul, tensorDistrib_tmul, associated_flip, associated_isSymm, QuadraticForm.associated_baseChange, LinearMap.dualProd.toQuadraticForm
instDistribMulActionOfSMulCommClass 📖	CompOp	—
instFunLike 📖	CompOp	118 math math: polar_zero_left, not_anisotropic_iff_exists, lineDeriv, sum_polar_sub_repr_sq, LinearMap.BilinMap.polar_toQuadraticMap, CliffordAlgebra.ι_mul_ι_mul_invOf_ι, CliffordAlgebra.isUnit_of_isUnit_ι, map_add_self, neg_apply, map_smul_of_tower, associated_eq_self_apply, polar_prod, sum_apply, linMulLin_apply, CliffordAlgebra.changeFormAux_changeFormAux, CliffordAlgebra.ι_mul_ι_comm, CliffordAlgebra.ι_sq_scalar, QuadraticForm.tmul_tensorMap_apply, polar_neg_left, ofPolar_apply, ext_iff, zero_apply, map_smul, associated_apply, map_zero, map_finsuppSum, comp_apply, isOrtho_def, polar_add_left, QuadraticForm.baseChange_tmul, proj_apply, CliffordAlgebra.ι_mul_ι_mul_ι, polar_smul_left_of_tower, toBilin_apply, evalAddMonoidHom_apply, polar_self, prod_apply, QuadraticForm.dualProd_apply, LinearMap.compQuadraticMap_polar, CliffordAlgebra.invOf_ι_mul_ι_mul_ι, CliffordAlgebra.EvenHom.contract, zeroHomClass, CliffordAlgebra.ι_mul_ι_add_swap, IsometryEquiv.map_app, coeFn_add, CliffordAlgebra.comp_ι_sq_scalar, map_sub, QuadraticForm.tmul_tensorAssoc_apply, Isometry.map_app, QuadraticForm.tmul_tensorComm_apply, QuadraticForm.tmul_tensorRId_apply, baseChange_ext_iff, CliffordAlgebra.EquivEven.Q'_apply, sub_apply, CliffordAlgebra.isUnit_ι_iff, smul_apply, PosDef.nonneg, coeFnAddMonoidHom_apply, map_finsuppSum', sq_apply, basisRepr_eq_of_iIsOrtho, QuadraticForm.tensorDistrib_tmul, polar_smul_left, pi_apply_single, PosDef.le_zero_iff, LinearMap.compQuadraticMap_apply, CliffordAlgebra.EquivEven.v_sq_scalar, map_add_add_add_map, lineDifferentiableAt, coeFn_sub, CliffordAlgebra.invOf_ι, QuadraticForm.tmul_tensorLId_apply, map_sum', map_neg, weightedSumSquares_apply, pi_apply, coeFn_neg, CliffordAlgebra.forall_mul_self_eq_iff, LinearMap.compQuadraticMap'_apply, Isometry.map_app', polar_neg_right, polar_sub_right, polar_add_right, apply_linearCombination', Anisotropic.eq_zero_iff, polar_sub_left, IsOrtho.polar_eq_zero, toFun_eq_coe, IsometryEquiv.map_app', polar_smul_right_of_tower, apply_linearCombination, coeFn_sum, CliffordAlgebraComplex.Q_apply, nonneg_prod_iff, nonneg_pi_iff, LinearMap.BilinMap.toQuadraticMap_apply, map_sum, posDef_iff_nonneg, sum_repr_sq_add_sum_repr_mul_polar, coeFn_zero, coe_mk, exists_companion, polarSym2_map_smul, coeFn_smul, tensorDistrib_tmul, Ring.polar_pi, CliffordAlgebra.GradedAlgebra.ι_sq_scalar, CliffordAlgebra.EvenHom.contract_mid, polar_smul_right, polar_zero_right, basisRepr_apply, restrictScalars_apply, CliffordAlgebra.contractLeftAux_contractLeftAux, CliffordAlgebraQuaternion.Q_apply, polarBilin_apply_apply, add_apply, congr_fun, hasLineDerivAt
instInhabited 📖	CompOp	—
instInvertibleEndOfNat 📖	CompOp	14 math math: canLift, associated_prod, associated_tmul, half_moduleEnd_apply_eq_half_smul, QuadraticForm.toDualProd_apply, associated_linMulLin, QuadraticForm.associated_isSymm, associated_sq, associated_isOrtho, Ring.associated_pi, CliffordAlgebra.changeForm.associated_neg_proof, separatingLeft_of_anisotropic, QuadraticForm.associated_tmul, QuadraticForm.associated_baseChange
instModuleOfSMulCommClass 📖	CompOp	33 math math: canLift, LinearEquiv.congrQuadraticMap_symm, toBilinHom_apply, associated_eq_self_apply, associated_rightInverse, LinearEquiv.congrQuadraticMap_refl, associated_prod, associated_apply, toQuadraticMap_associated, associated_left_inverse, associated_tmul, associated_toQuadraticMap, two_nsmul_associated, associated_left_inverse', LinearMap.BilinMap.toQuadraticMapLinearMap_apply, QuadraticForm.tensorDistrib_tmul, QuadraticForm.toDualProd_apply, canLift', coe_associatedHom, LinearEquiv.congrQuadraticMap_symm_apply, associated_linMulLin, QuadraticForm.associated_isSymm, associated_sq, associated_comp, associated_isOrtho, Ring.associated_pi, CliffordAlgebra.changeForm.associated_neg_proof, LinearEquiv.congrQuadraticMap_apply, QuadraticForm.associated_tmul, tensorDistrib_tmul, associated_flip, associated_isSymm, QuadraticForm.associated_baseChange
instNeg 📖	CompOp	7 math math: neg_apply, QuadraticForm.toDualProd_apply, coeFn_neg, CliffordAlgebra.evenEquivEvenNeg_apply, CliffordAlgebra.evenEquivEvenNeg_symm_apply, CliffordAlgebra.changeForm.associated_neg_proof, LinearMap.BilinMap.toQuadraticMap_neg
instSMul 📖	CompOp	9 math math: smul_toBilin, instIsScalarTower, discr_smul, instSMulCommClass, smul_apply, LinearMap.BilinMap.toQuadraticMap_smul, PosDef.smul, coeFn_smul, toMatrix'_smul
instSub 📖	CompOp	5 math math: CliffordAlgebra.changeForm.zero_proof, sub_apply, coeFn_sub, CliffordAlgebra.changeForm.associated_neg_proof, LinearMap.BilinMap.toQuadraticMap_sub
instZero 📖	CompOp	139 math math: ExteriorAlgebra.isLocalHom_algebraMap, ExteriorAlgebra.GradedAlgebra.liftι_eq, ExteriorAlgebra.ι_eq_algebraMap_iff, exteriorPower.basis_apply, ExteriorAlgebra.ι_inj, exteriorPower.linearMap_ext_iff, ExteriorAlgebra.lift_symm_apply, exteriorPower.coe_basis, exteriorPower.ιMulti_family_linearIndependent_field, exteriorPower.basis_repr_ne, CliffordAlgebraDualNumber.equiv_symm_eps, ExteriorAlgebra.ιMulti_span_fixedDegree, Isometry.proj_comp_single_of_same, ExteriorAlgebra.ι_eq_zero_iff, ExteriorAlgebra.map_comp_map, exteriorPower.ιMulti_family_span_fixedDegree_of_span, LinearMap.BilinMap.toQuadraticMap_zero, ExteriorAlgebra.liftAlternating_ι_mul, ExteriorAlgebra.toTrivSqZeroExt_comp_map, exteriorPower.alternatingMapLinearEquiv_ιMulti, ExteriorAlgebra.algebraMap_inj, ExteriorAlgebra.algebraMap_eq_one_iff, ExteriorAlgebra.liftAlternating_comp, exteriorPower.ιMulti_span_of_span, exteriorPower.alternatingMapLinearEquiv_symm_map, exteriorPower.instFree, ExteriorAlgebra.ιMulti_succ_apply, ExteriorAlgebra.map_comp_ι, ExteriorAlgebra.ιMulti_span, ExteriorAlgebra.map_comp_ιMulti, exteriorPower.ιMultiDual_apply_diag, ExteriorAlgebra.algebraMap_eq_zero_iff, ExteriorAlgebra.lift_ι_apply, ExteriorAlgebra.ιMulti_zero_apply, zero_apply, TensorAlgebra.toExterior_ι, ExteriorAlgebra.liftAlternatingEquiv_symm_apply, LinearMap.BilinMap.toQuadraticMap_eq_zero, ExteriorAlgebra.GradedAlgebra.ι_sq_zero, ExteriorAlgebra.lift_comp_ι, ExteriorAlgebra.liftAlternating_ιMulti, Isometry.snd_comp_inl, ExteriorAlgebra.liftAlternatingEquiv_apply, IsOrtho.all, ExteriorAlgebra.ι_comp_lift, exteriorPower.finrank_eq, Isometry.snd_apply, ExteriorAlgebra.invertibleAlgebraMapEquiv_apply_invOf, exteriorPower.map_apply_ιMulti_family, ExteriorAlgebra.ιMulti_range, exteriorPower.zeroEquiv_naturality, ExteriorAlgebra.liftAlternating_apply_ιMulti, exteriorPower.ιMulti_span_fixedDegree_of_span_eq_top, exteriorPower.ιMulti_apply_coe, exteriorPower.oneEquiv_naturality, ExteriorAlgebra.ι_range_disjoint_one, ExteriorAlgebra.liftAlternating_one, ExteriorAlgebra.ι_sq_zero, exteriorPower.alternatingMapLinearEquiv_apply_ιMulti, exteriorPower.ιMultiDual_apply_ιMulti, Isometry.proj_comp_single_of_ne, exteriorPower.ιMulti_family_eq_coe_comp, exteriorPower.pairingDual_ιMulti_ιMulti, ExteriorAlgebra.map_apply_ι, ExteriorAlgebra.ι_leftInverse, exteriorPower.alternatingMapLinearEquiv_comp_ιMulti, exteriorPower.oneEquiv_symm_apply, exteriorPower.map_comp_ιMulti, ExteriorAlgebra.instGradedMonoidNatSubmoduleExteriorPower, ExteriorAlgebra.ι_add_mul_swap, exteriorPower.pairingDual_apply_apply_eq_one, ExteriorAlgebra.toTrivSqZeroExt_ι, LinearMap.BilinMap.toQuadraticMap_list_sum, ExteriorAlgebra.isUnit_algebraMap, ExteriorAlgebra.map_injective_field, ExteriorAlgebra.map_injective, exteriorPower.ιMulti_family_span_of_span, exteriorPower.map_injective_field, Isometry.proj_apply, ExteriorAlgebra.ιMulti_apply, Isometry.fst_apply, exteriorPower.alternatingMapLinearEquiv_comp, exteriorPower.basis_coord, exteriorPower.presentation_relation, Isometry.fst_comp_inl, exteriorPower.instFinite, exteriorPower.alternatingMapToDual_apply_ιMulti, ExteriorAlgebra.map_surjective_iff, CliffordAlgebraRing.ι_eq_zero, exteriorPower.zeroEquiv_ιMulti, ExteriorAlgebra.liftAlternating_comp_ιMulti, CliffordAlgebraRing.involute_eq_id, exteriorPower.map_injective, exteriorPower.basis_repr_apply, exteriorPower.presentation_R, CliffordAlgebraDualNumber.equiv_ι, Isometry.fst_comp_inr, ExteriorAlgebra.algebraMap_leftInverse, exteriorPower.map_comp_ιMulti_family, exteriorPower.map_id, ExteriorAlgebra.map_apply_ιMulti, exteriorPower.pairingDual_apply_apply_eq_one_zero, ExteriorAlgebra.lift_unique, CliffordAlgebraRing.reverse_apply, ExteriorAlgebra.hom_ext_iff, ExteriorAlgebra.liftAlternating_algebraMap, ExteriorAlgebra.map_id, CliffordAlgebraDualNumber.ι_mul_ι, exteriorPower.basis_repr, exteriorPower.alternatingMapLinearEquiv_symm_apply, ExteriorAlgebra.ιInv_comp_map, CliffordAlgebra.changeForm.associated_neg_proof, exteriorPower.map_apply_ιMulti, ExteriorAlgebra.lhom_ext_iff, ExteriorAlgebra.ι_range_map_map, exteriorPower.map_comp, exteriorPower.ιMultiDual_apply_nondiag, exteriorPower.presentation_var, ExteriorAlgebra.comp_ι_sq_zero, exteriorPower.map_surjective, coeFn_zero, ExteriorAlgebra.ι_mul_prod_list, ExteriorAlgebra.ιMulti_succ_curryLeft, ExteriorAlgebra.leftInverse_map_iff, exteriorPower.presentation_G, exteriorPower.ιMulti_family_linearIndependent_ofBasis, exteriorPower.ιMulti_family_span, exteriorPower.ιMulti_span_fixedDegree, CliffordAlgebraRing.reverse_eq_id, ExteriorAlgebra.GradedAlgebra.ι_apply, ExteriorAlgebra.invertibleAlgebraMapEquiv_symm_apply_invOf_toQuot, exteriorPower.oneEquiv_ιMulti, exteriorPower.ιMulti_span, exteriorPower.toTensorPower_apply_ιMulti, exteriorPower.zeroEquiv_symm_apply, ExteriorAlgebra.liftAlternating_ι, exteriorPower.ιMulti_family_apply_coe, exteriorPower.basis_repr_self, Isometry.snd_comp_inr
linMulLin 📖	CompOp	6 math math: linMulLinSelfPosDef, add_linMulLin, linMulLin_apply, associated_linMulLin, linMulLin_comp, linMulLin_add
ofPolar 📖	CompOp	1 math math: ofPolar_apply
polar 📖	CompOp	36 math math: polar_zero_left, lineDeriv, LinearMap.BilinMap.polar_toQuadraticMap, CliffordAlgebra.ι_mul_ι_mul_invOf_ι, polar_add_left_iff, polar_add, polar_prod, CliffordAlgebra.ι_mul_ι_comm, polar_neg_left, CliffordAlgebra.mul_add_swap_eq_polar_of_forall_mul_self_eq, polar_smul, polar_add_left, polar_comm, CliffordAlgebra.ι_mul_ι_mul_ι, polar_smul_left_of_tower, toBilin_apply, polar_self, map_add, LinearMap.compQuadraticMap_polar, CliffordAlgebra.invOf_ι_mul_ι_mul_ι, CliffordAlgebra.ι_mul_ι_add_swap, polar_smul_left, polarSym2_sym2Mk, polar_comp, polar_neg, polar_neg_right, polar_sub_right, polar_add_right, polar_sub_left, IsOrtho.polar_eq_zero, polar_smul_right_of_tower, Ring.polar_pi, polar_smul_right, polar_zero_right, polarBilin_apply_apply, hasLineDerivAt
polarBilin 📖	CompOp	14 math math: polarBilin_prod, QuadraticForm.polarBilin_baseChange, QuadraticForm.polarBilin_tmul, Ring.polarBilin_pi, polarBilin_injective, choose_exists_companion, two_nsmul_associated, isOrtho_polarBilin, toQuadraticMap_polarBilin, CliffordAlgebra.forall_mul_self_eq_iff, LinearMap.compQuadraticMap_polarBilin, LinearMap.BilinMap.polarBilin_toQuadraticMap, polarBilin_comp, polarBilin_apply_apply
polarSym2 📖	CompOp	10 math math: sum_polar_sub_repr_sq, map_finsuppSum, map_finsuppSum', polarSym2_sym2Mk, map_sum', apply_linearCombination', apply_linearCombination, map_sum, sum_repr_sq_add_sum_repr_mul_polar, polarSym2_map_smul
proj 📖	CompOp	1 math math: proj_apply
restrictScalars 📖	CompOp	1 math math: restrictScalars_apply
sq 📖	CompOp	16 math math: QuadraticForm.tensorRId_symm_apply, QuadraticForm.tensorRId_apply, QuadraticForm.comp_tensorLId_eq, QuadraticForm.tensorLId_toLinearEquiv, QuadraticForm.tmul_tensorRId_apply, QuadraticModuleCat.toIsometry_hom_leftUnitor, QuadraticModuleCat.toIsometry_hom_rightUnitor, QuadraticForm.tensorLId_symm_apply, sq_apply, QuadraticModuleCat.toIsometry_inv_rightUnitor, QuadraticForm.tensorRId_toLinearEquiv, QuadraticForm.tmul_tensorLId_apply, QuadraticForm.tensorLId_apply, QuadraticForm.comp_tensorRId_eq, associated_sq, QuadraticModuleCat.toIsometry_inv_leftUnitor
toFun 📖	CompOp	3 math math: toFun_smul, exists_companion', toFun_eq_coe
toMatrix' 📖	CompOp	4 math math: QuadraticForm.posDef_toMatrix', toMatrix'_comp, isSymm_toMatrix', toMatrix'_smul
weightedSumSquares 📖	CompOp	9 math math: QuadraticForm.equivalent_signType_weighted_sum_squared, QuadraticForm.equivalent_one_neg_one_weighted_sum_squared, QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared, QuadraticForm.equivalent_weightedSumSquares, basisRepr_eq_of_iIsOrtho, QuadraticForm.equivalent_sum_squares, weightedSumSquares_apply, QuadraticForm.equivalent_sign_ne_zero_weighted_sum_squared, QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	DFunLike.coe QuadraticMap instFunLike instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
add_linMulLin 📖	mathematical	—	linMulLin LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid LinearMap.instAdd QuadraticMap instAdd	—	ext add_mul Distrib.rightDistribClass
associated_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LinearMap.BilinMap LinearMap.addCommMonoid LinearMap.module QuadraticMap instAddCommMonoid instModuleOfSMulCommClass IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction associatedHom Module.End SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass Module.End.instMonoid Module.End.instSemiring Module.End.applyModule Invertible.invOf Module.End.instMul Module.End.instOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Module.End.instRing Nat.instAtLeastTwoHAddOfNat SubNegMonoid.toSub instFunLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass
associated_comp 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.BilinMap instAddCommMonoid LinearMap.addCommMonoid LinearMap.module instModuleOfSMulCommClass IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike associatedHom comp LinearMap.compl₁₂	—	Nat.instAtLeastTwoHAddOfNat LinearMap.ext IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass
associated_eq_self_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LinearMap.BilinMap LinearMap.addCommMonoid LinearMap.module QuadraticMap instAddCommMonoid instModuleOfSMulCommClass IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction associatedHom instFunLike	—	Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass associated_apply map_add_self three_add_one_eq_four two_add_one_eq_three add_smul one_smul add_sub_cancel_right two_smul invOf_smul_eq_iff
associated_flip 📖	mathematical	—	LinearMap.flip CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearMap QuadraticMap LinearMap.BilinMap instAddCommMonoid LinearMap.addCommMonoid LinearMap.module instModuleOfSMulCommClass IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike associatedHom	—	Nat.instAtLeastTwoHAddOfNat LinearMap.ext SMulCommClass.symm IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass add_comm sub_eq_add_neg add_left_comm add_assoc
associated_isOrtho 📖	mathematical	—	LinearMap.IsOrtho CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe LinearMap QuadraticMap LinearMap.BilinMap instAddCommMonoid LinearMap.addCommMonoid LinearMap.module instModuleOfSMulCommClass smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike associated instInvertibleEndOfNat IsOrtho	—	Nat.instAtLeastTwoHAddOfNat smulCommClass_self LinearMap.instSMulCommClass smul_zero sub_sub
associated_isSymm 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LinearMap.BilinMap LinearMap.addCommMonoid LinearMap.module QuadraticMap instAddCommMonoid instModuleOfSMulCommClass IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction associatedHom	—	Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass sub_eq_add_neg add_assoc add_comm add_left_comm
associated_left_inverse 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LinearMap.BilinMap LinearMap.addCommMonoid LinearMap.module	QuadraticMap instAddCommMonoid instModuleOfSMulCommClass IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction associatedHom LinearMap.BilinMap.toQuadraticMap	—	Nat.instAtLeastTwoHAddOfNat LinearMap.ext₂ IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass associated_toQuadraticMap two_smul invOf_smul_eq_iff
associated_left_inverse' 📖	mathematical	LinearMap.flip CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring	DFunLike.coe LinearMap QuadraticMap LinearMap.BilinMap instAddCommMonoid LinearMap.addCommMonoid LinearMap.module instModuleOfSMulCommClass IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike associatedHom LinearMap.BilinMap.toQuadraticMap	—	Nat.instAtLeastTwoHAddOfNat SMulCommClass.symm LinearMap.ext IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass associated_toQuadraticMap LinearMap.flip_apply invOf_smul_eq_iff two_smul
associated_linMulLin 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring QuadraticMap AddCommGroup.toAddCommMonoid Ring.toAddCommGroup CommRing.toRing Semiring.toModule LinearMap.BilinMap instAddCommMonoid LinearMap.addCommMonoid LinearMap.module instModuleOfSMulCommClass smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike associated instInvertibleEndOfNat linMulLin NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.to_smulCommClass Algebra.id IsScalarTower.right NonUnitalNonAssocSemiring.toAddCommMonoid CommSemiring.toCommMonoid LinearMap.instSMul LinearMap.instDistribMulAction Invertible.invOf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat LinearMap.instAdd LinearMap.compl₁₂ LinearMap.mul	—	Nat.instAtLeastTwoHAddOfNat LinearMap.ext smulCommClass_self LinearMap.instSMulCommClass Algebra.to_smulCommClass IsScalarTower.right map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass smul_add nsmul_eq_mul mul_invOf_cancel_left' Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero
associated_rightInverse 📖	mathematical	—	LinearMap.BilinMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid QuadraticMap DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid LinearMap.addCommMonoid LinearMap.module instModuleOfSMulCommClass IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike associatedHom LinearMap.BilinMap.toQuadraticMap	—	Nat.instAtLeastTwoHAddOfNat toQuadraticMap_associated
associated_sq 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring QuadraticMap AddCommGroup.toAddCommMonoid Ring.toAddCommGroup CommRing.toRing Semiring.toModule LinearMap.BilinMap instAddCommMonoid LinearMap.addCommMonoid LinearMap.module instModuleOfSMulCommClass smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike associated instInvertibleEndOfNat sq NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.to_smulCommClass Algebra.id IsScalarTower.right LinearMap.mul	—	Nat.instAtLeastTwoHAddOfNat smulCommClass_self LinearMap.instSMulCommClass Algebra.to_smulCommClass IsScalarTower.right associated_linMulLin smul_add invOf_two_smul_add_invOf_two_smul
associated_toQuadraticMap 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LinearMap.BilinMap LinearMap.addCommMonoid LinearMap.module QuadraticMap instAddCommMonoid instModuleOfSMulCommClass IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction associatedHom LinearMap.BilinMap.toQuadraticMap Module.End SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass Module.End.instMonoid Module.End.instSemiring Module.End.applyModule Invertible.invOf Module.End.instMul Module.End.instOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Module.End.instRing Nat.instAtLeastTwoHAddOfNat AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg add_zero Mathlib.Tactic.Abel.zero_termg Mathlib.Tactic.Abel.termg_eq one_zsmul Mathlib.Tactic.Abel.const_add_termg
basisRepr_apply 📖	mathematical	—	DFunLike.coe QuadraticMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule instFunLike basisRepr Finite.of_fintype Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Module.Basis Module.Basis.instFunLike	—	Finite.of_fintype RingHomInvPair.ids Module.Basis.equivFun_symm_apply
basisRepr_eq_of_iIsOrtho 📖	mathematical	LinearMap.IsOrthoᵢ CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearMap QuadraticMap LinearMap.BilinMap instAddCommMonoid LinearMap.addCommMonoid LinearMap.module instModuleOfSMulCommClass smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike associated instInvertibleEndOfNat Module.Basis Module.Basis.instFunLike	basisRepr NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Finite.of_fintype weightedSumSquares NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.to_smulCommClass Algebra.id QuadraticForm instFunLike	—	Nat.instAtLeastTwoHAddOfNat smulCommClass_self LinearMap.instSMulCommClass ext Finite.of_fintype Algebra.to_smulCommClass basisRepr_apply IsScalarTower.to_smulCommClass IsScalarTower.right IsScalarTower.to_smulCommClass' associated_eq_self_apply map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass weightedSumSquares_apply Finset.sum_congr LinearMap.map_sum₂ Finset.sum_eq_single_of_mem map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.map_smul₂ Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.zero_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap smul_eq_mul associated_apply Module.End.smul_def half_moduleEnd_apply_eq_half_smul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg add_zero Mathlib.Tactic.RingNF.add_neg Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add
canLift 📖	mathematical	—	CanLift LinearMap.BilinMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring QuadraticForm DFunLike.coe LinearMap Nat.instCommSemiring RingHom.id Semiring.toNonAssocSemiring QuadraticMap Ring.toAddCommGroup CommRing.toRing instAddCommMonoid LinearMap.addCommMonoid LinearMap.module instModuleOfSMulCommClass AddCommMonoid.toNatModule IsScalarTower.to_smulCommClass Semiring.toNatAlgebra IsScalarTower.right IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike associatedHom instInvertibleEndOfNat LinearMap.IsSymm	—	Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass IsScalarTower.right IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass Algebra.to_smulCommClass associated_left_inverse
canLift' 📖	mathematical	—	CanLift LinearMap.BilinMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid QuadraticMap DFunLike.coe LinearMap CommSemiring.toSemiring Nat.instCommSemiring RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid LinearMap.addCommMonoid LinearMap.module instModuleOfSMulCommClass AddCommMonoid.toNatModule IsScalarTower.to_smulCommClass Semiring.toNatAlgebra AddCommMonoid.nat_isScalarTower IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike associatedHom SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass LinearMap.flip	—	Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass AddCommMonoid.nat_isScalarTower IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass SMulCommClass.symm associated_left_inverse'
choose_exists_companion 📖	mathematical	—	LinearMap.BilinMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid exists_companion polarBilin	—	LinearMap.ext₂ exists_companion polarBilin_apply_apply polar.eq_1 sub_sub add_sub_cancel_left
coeFnAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom QuadraticMap AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid Pi.addZeroClass AddMonoidHom.instFunLike coeFnAddMonoidHom instFunLike	—	—
coeFn_add 📖	mathematical	—	DFunLike.coe QuadraticMap instFunLike instAdd Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
coeFn_neg 📖	mathematical	—	DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike instNeg Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
coeFn_smul 📖	mathematical	—	DFunLike.coe QuadraticMap instFunLike instSMul Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—
coeFn_sub 📖	mathematical	—	DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike instSub Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
coeFn_sum 📖	mathematical	—	DFunLike.coe QuadraticMap instFunLike Finset.sum instAddCommMonoid Pi.addCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass
coeFn_zero 📖	mathematical	—	DFunLike.coe QuadraticMap instFunLike instZero Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
coe_associatedHom 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.BilinMap instAddCommMonoid LinearMap.addCommMonoid LinearMap.module instModuleOfSMulCommClass IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike associatedHom smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing associated	—	Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass
coe_copy 📖	mathematical	DFunLike.coe QuadraticMap instFunLike	copy	—	—
coe_mk 📖	mathematical	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike LinearMap.BilinMap LinearMap.addCommMonoid LinearMap.module	QuadraticMap instFunLike	—	—
comp_apply 📖	mathematical	—	DFunLike.coe QuadraticMap instFunLike comp LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	—
congr_fun 📖	mathematical	—	DFunLike.coe QuadraticMap instFunLike	—	DFunLike.congr_fun
copy_eq 📖	mathematical	DFunLike.coe QuadraticMap instFunLike	copy	—	DFunLike.ext'
discr_comp 📖	mathematical	—	discr comp CommRing.toCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module CommSemiring.toSemiring Semiring.toModule Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Matrix.det DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonAssocSemiring.toNonUnitalNonAssocSemiring Matrix LinearMap.addCommMonoid Matrix.addCommMonoid LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix'	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass Matrix.det.congr_simp toMatrix'_comp Matrix.det_mul Matrix.det_transpose mul_comm mul_left_comm
discr_smul 📖	mathematical	—	discr QuadraticMap CommRing.toCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module CommSemiring.toSemiring Semiring.toModule instSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow Fintype.card	—	Nat.instAtLeastTwoHAddOfNat Algebra.to_smulCommClass Matrix.det.congr_simp toMatrix'_smul Matrix.det_smul
evalAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom QuadraticMap AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid AddMonoidHom.instFunLike evalAddMonoidHom instFunLike	—	—
exists_companion 📖	mathematical	—	DFunLike.coe QuadraticMap instFunLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.BilinMap LinearMap.addCommMonoid LinearMap.module	—	exists_companion'
exists_companion' 📖	mathematical	—	toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.BilinMap LinearMap.addCommMonoid LinearMap.module	—	—
exists_quadraticMap_ne_zero 📖	—	—	—	—	Nat.instAtLeastTwoHAddOfNat ext map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
ext 📖	—	DFunLike.coe QuadraticMap instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe QuadraticMap instFunLike	—	ext
half_moduleEnd_apply_eq_half_smul 📖	mathematical	—	DFunLike.coe Module.End LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Invertible.invOf Module.End.instMul Module.End.instOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Module.End.instSemiring Nat.instAtLeastTwoHAddOfNat instInvertibleEndOfNat SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne	—	Nat.instAtLeastTwoHAddOfNat
instIsScalarTower 📖	mathematical	—	IsScalarTower QuadraticMap instSMul	—	ext smul_assoc
instSMulCommClass 📖	mathematical	—	SMulCommClass QuadraticMap instSMul	—	ext SMulCommClass.smul_comm
isOrtho_comm 📖	mathematical	—	IsOrtho	—	add_comm
isOrtho_def 📖	mathematical	—	IsOrtho DFunLike.coe QuadraticMap instFunLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
isOrtho_polarBilin 📖	mathematical	—	LinearMap.IsOrtho CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring polarBilin IsOrtho	—	smulCommClass_self sub_sub
isSymm_toMatrix' 📖	mathematical	—	Matrix.IsSymm toMatrix'	—	Nat.instAtLeastTwoHAddOfNat Matrix.ext toMatrix'.eq_1 Matrix.transpose_apply RingHomInvPair.ids LinearMap.instSMulCommClass LinearMap.toMatrix₂'_apply IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' associated_isSymm
linMulLinSelfPosDef 📖	mathematical	LinearMap.ker CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring RingHom.id Bot.bot Submodule Submodule.instBot	PosDef SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linMulLin	—	mul_self_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toMulPosStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing contravariant_lt_of_covariant_le LinearMap.ker_eq_bot'
linMulLin_add 📖	mathematical	—	linMulLin LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid LinearMap.instAdd QuadraticMap instAdd	—	ext mul_add Distrib.leftDistribClass
linMulLin_apply 📖	mathematical	—	DFunLike.coe QuadraticMap NonUnitalNonAssocSemiring.toAddCommMonoid instFunLike linMulLin Distrib.toMul NonUnitalNonAssocSemiring.toDistrib LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	—
linMulLin_comp 📖	mathematical	—	comp NonUnitalNonAssocSemiring.toAddCommMonoid linMulLin LinearMap.comp CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	—
map_add 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid polar	—	polar.eq_1 Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.const_add_termg Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.zero_termg
map_add_add_add_map 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup DFunLike.coe QuadraticMap instFunLike	—	exists_companion add_comm LinearMap.map_add₂ Mathlib.Tactic.Abel.subst_into_add Mathlib.Tactic.Abel.term_atom Mathlib.Tactic.Abel.term_add_const zero_add Mathlib.Tactic.Abel.term_add_term Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat add_zero Mathlib.Tactic.Abel.const_add_term
map_add_self 📖	mathematical	—	DFunLike.coe QuadraticMap instFunLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddMonoid.toNatSMul AddCommMonoid.toAddMonoid	—	Nat.instAtLeastTwoHAddOfNat two_smul map_smul Nat.cast_smul_eq_nsmul Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_natCast
map_neg 📖	mathematical	—	DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	neg_one_smul map_smul neg_one_mul neg_neg one_smul
map_smul 📖	mathematical	—	DFunLike.coe QuadraticMap instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	toFun_smul
map_smul_of_tower 📖	mathematical	—	DFunLike.coe QuadraticMap instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	IsScalarTower.algebraMap_smul map_smul map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass algebraMap_smul
map_sub 📖	mathematical	—	DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	neg_sub map_neg
map_sum 📖	mathematical	—	DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike Finset.sum AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Sym2 Finset.filter Sym2.IsDiag Sym2.IsDiag.decidablePred Finset.sym2 polarSym2 Sym2.map	—	Finset.cons_induction map_zero zeroHomClass Finset.sum_congr Finset.filter_empty add_zero Finset.sum_cons map_add add_assoc Finset.filter.congr_simp Finset.sym2_cons Finset.sum_filter Finset.sum_disjUnion Finset.sum_map zero_add map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass add_comm
map_sum' 📖	mathematical	—	DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike Finset.sum SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Sym2 Finset.sym2 polarSym2 Sym2.map	—	Finset.cons_induction map_zero zeroHomClass sub_self Finset.sum_cons map_add add_assoc Finset.sum_congr Finset.sym2_cons Finset.sum_disjUnion Finset.sum_map map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass polar_self Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.termg_eq one_zsmul add_zero Mathlib.Tactic.Abel.subst_into_smul_upcast Mathlib.Tactic.Abel.term_smulg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.zero_smulg Mathlib.Tactic.Abel.const_add_termg Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isInt_neg
map_zero 📖	mathematical	—	DFunLike.coe QuadraticMap instFunLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	zero_smul map_smul MulZeroClass.zero_mul
ne_zero_of_not_isOrtho_self 📖	—	IsOrtho	—	—	IsOrtho.zero_left
neg_apply 📖	mathematical	—	DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
not_anisotropic_iff_exists 📖	mathematical	—	Anisotropic DFunLike.coe QuadraticMap instFunLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
ofPolar_apply 📖	mathematical	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing polar AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	DFunLike.coe QuadraticMap instFunLike ofPolar	—	—
polarBilin_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module polarBilin polar QuadraticMap instFunLike	—	—
polarBilin_comp 📖	mathematical	—	polarBilin comp CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.compl₁₂ CommSemiring.toSemiring	—	LinearMap.ext₂ map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass
polarBilin_injective 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	QuadraticMap AddCommGroup.toAddCommMonoid LinearMap.BilinMap polarBilin	—	Nat.instAtLeastTwoHAddOfNat smulCommClass_self IsUnit.smul_left_cancel Nat.cast_smul_eq_nsmul
polarSym2_map_smul 📖	mathematical	—	polarSym2 DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike Sym2.map Pi.smul' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction Sym2.mul NonUnitalNonAssocCommSemiring.toCommMagma NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Sym2.map_congr polar_smul_right polar_smul_left IsScalarTower.left mul_comm
polarSym2_sym2Mk 📖	mathematical	—	polarSym2 polar	—	—
polar_add 📖	mathematical	—	polar Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.const_add_termg
polar_add_left 📖	mathematical	—	polar DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	polar_add_left_iff map_add_add_add_map
polar_add_left_iff 📖	mathematical	—	polar AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	add_sub sub_add_eq_add_sub add_right_comm add_comm AddRightCancelSemigroup.toIsRightCancelAdd
polar_add_right 📖	mathematical	—	polar DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	polar_comm polar_add_left
polar_comm 📖	mathematical	—	polar	—	polar.eq_1 add_comm sub_sub
polar_comp 📖	mathematical	—	polar DFunLike.coe	—	map_sub
polar_neg 📖	mathematical	—	polar Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	sub_eq_add_neg neg_add
polar_neg_left 📖	mathematical	—	polar DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	neg_one_smul polar_smul_left
polar_neg_right 📖	mathematical	—	polar DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	neg_one_smul polar_smul_right
polar_self 📖	mathematical	—	polar DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	polar.eq_1 map_add_self sub_sub sub_eq_iff_eq_add Nat.instAtLeastTwoHAddOfNat two_smul SemigroupAction.mul_smul
polar_smul 📖	mathematical	—	polar Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	smul_sub
polar_smul_left 📖	mathematical	—	polar DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	—	exists_companion map_smul LinearMap.map_smul₂ sub_sub add_sub_cancel_left
polar_smul_left_of_tower 📖	mathematical	—	polar DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	—	IsScalarTower.algebraMap_smul polar_smul_left algebraMap_smul
polar_smul_right 📖	mathematical	—	polar DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	—	polar_comm polar_smul_left
polar_smul_right_of_tower 📖	mathematical	—	polar DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	—	IsScalarTower.algebraMap_smul polar_smul_right algebraMap_smul
polar_sub_left 📖	mathematical	—	polar DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_eq_add_neg polar_add_left polar_neg_left
polar_sub_right 📖	mathematical	—	polar DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_eq_add_neg polar_add_right polar_neg_right
polar_zero_left 📖	mathematical	—	polar DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	zero_add map_zero sub_zero sub_self
polar_zero_right 📖	mathematical	—	polar DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	add_zero sub_self map_zero
posDef_iff_nonneg 📖	mathematical	—	PosDef Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe QuadraticMap instFunLike Anisotropic	—	PosDef.nonneg PosDef.anisotropic posDef_of_nonneg
posDef_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe QuadraticMap instFunLike Anisotropic	PosDef	—	lt_of_le_of_ne
proj_apply 📖	mathematical	—	DFunLike.coe QuadraticMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Pi.Function.module CommSemiring.toSemiring instFunLike proj Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
restrictScalars_apply 📖	mathematical	—	DFunLike.coe QuadraticMap instFunLike restrictScalars	—	—
separatingLeft_of_anisotropic 📖	mathematical	Anisotropic CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring	LinearMap.SeparatingLeft Ring.toAddCommGroup CommRing.toRing RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearMap Int.instSemiring QuadraticMap LinearMap.BilinMap instAddCommMonoid LinearMap.addCommMonoid LinearMap.module AddCommGroup.toIntModule instAddCommGroup LinearMap.addCommGroup LinearMap.instFunLike associated' instInvertibleEndOfNat	—	Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass associated_eq_self_apply
smul_apply 📖	mathematical	—	DFunLike.coe QuadraticMap instFunLike instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—
sq_apply 📖	mathematical	—	DFunLike.coe QuadraticMap NonUnitalNonAssocSemiring.toAddCommMonoid instFunLike sq Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
sub_apply 📖	mathematical	—	DFunLike.coe QuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
sum_apply 📖	mathematical	—	DFunLike.coe QuadraticMap instFunLike Finset.sum instAddCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass
toFun_eq_coe 📖	mathematical	—	toFun DFunLike.coe QuadraticMap instFunLike	—	—
toFun_smul 📖	mathematical	—	toFun SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—
toMatrix'_comp 📖	mathematical	—	toMatrix' comp CommRing.toCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module CommSemiring.toSemiring Semiring.toModule Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Matrix.transpose DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid Matrix.addCommMonoid LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix'	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass LinearMap.instSMulCommClass IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' associated_comp LinearMap.toMatrix₂'_compl₁₂
toMatrix'_smul 📖	mathematical	—	toMatrix' QuadraticMap CommRing.toCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module CommSemiring.toSemiring Semiring.toModule instSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Matrix Matrix.smul Algebra.toSMul	—	Nat.instAtLeastTwoHAddOfNat Algebra.to_smulCommClass LinearMap.instSMulCommClass map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass
toQuadraticMap_associated 📖	mathematical	—	LinearMap.BilinMap.toQuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring QuadraticMap LinearMap.BilinMap instAddCommMonoid LinearMap.addCommMonoid LinearMap.module instModuleOfSMulCommClass IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike associatedHom	—	Nat.instAtLeastTwoHAddOfNat ext IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass associated_eq_self_apply
toQuadraticMap_polarBilin 📖	mathematical	—	LinearMap.BilinMap.toQuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid polarBilin QuadraticMap AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup	—	ext polar_self
two_nsmul_associated 📖	mathematical	—	LinearMap.BilinMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LinearMap.addCommGroup LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.module DFunLike.coe QuadraticMap instAddCommMonoid LinearMap.addCommMonoid instModuleOfSMulCommClass IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike associatedHom polarBilin	—	Nat.instAtLeastTwoHAddOfNat LinearMap.ext IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass AddMonoid.nat_smulCommClass' LinearMap.smul_apply nsmul_eq_mul Nat.cast_ofNat mul_invOf_self' Module.End.one_apply polar.eq_1
weightedSumSquares_apply 📖	mathematical	—	DFunLike.coe QuadraticMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule instFunLike weightedSumSquares Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	sum_apply
zeroHomClass 📖	mathematical	—	ZeroHomClass QuadraticMap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike	—	map_zero
zero_apply 📖	mathematical	—	DFunLike.coe QuadraticMap instFunLike instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—

QuadraticMap.Anisotropic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_iff 📖	mathematical	QuadraticMap.Anisotropic	DFunLike.coe QuadraticMap QuadraticMap.instFunLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	map_zero QuadraticMap.zeroHomClass

QuadraticMap.IsOrtho

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
all 📖	mathematical	—	QuadraticMap.IsOrtho QuadraticMap QuadraticMap.instZero	—	zero_add
polar_eq_zero 📖	mathematical	QuadraticMap.IsOrtho CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	QuadraticMap.polar DFunLike.coe QuadraticMap QuadraticMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	QuadraticMap.isOrtho_polarBilin
zero_left 📖	mathematical	—	QuadraticMap.IsOrtho AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	zero_add map_zero QuadraticMap.zeroHomClass
zero_right 📖	mathematical	—	QuadraticMap.IsOrtho AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	add_zero map_zero QuadraticMap.zeroHomClass

QuadraticMap.PosDef

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	QuadraticMap.PosDef	QuadraticMap QuadraticMap.instAdd	—	add_pos
anisotropic 📖	mathematical	QuadraticMap.PosDef	QuadraticMap.Anisotropic	—	by_contradiction lt_irrefl
le_zero_iff 📖	mathematical	QuadraticMap.PosDef	Preorder.toLE PartialOrder.toPreorder DFunLike.coe QuadraticMap QuadraticMap.instFunLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	le_antisymm nonneg anisotropic map_zero QuadraticMap.zeroHomClass
nonneg 📖	mathematical	QuadraticMap.PosDef	Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe QuadraticMap QuadraticMap.instFunLike	—	eq_or_ne Eq.le map_zero QuadraticMap.zeroHomClass LT.lt.le
smul 📖	mathematical	QuadraticMap.PosDef Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	QuadraticMap QuadraticMap.instSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid	—	smul_pos

---

← Back to Index