Properties

📁 Source: Mathlib/LinearAlgebra/BilinearForm/Properties.lean

Statistics

Metric	Count
Definitions IsAlt, IsNonneg, IsPosSemidef, IsRefl, IsSymm, dualBasis, leftAdjointOfNondegenerate, symmCompOfNondegenerate, toDual	9
Theorems add, eq_of_add_add_eq_zero, isRefl, neg, neg_eq, self_eq_zero, smul, sub, add, nonneg, smul, add, isNonneg, isSymm, smul, eq_zero, groupSMul, neg, smul, add, eq, isRefl, neg, polarization, restrict, smul, sub, flip, ker_eq_bot, ne_zero, apply_dualBasis_left, apply_dualBasis_right, apply_toDual_symm_apply, compLeft_injective, comp_symmCompOfNondegenerate_apply, dualBasis_dualBasis, dualBasis_dualBasis_flip, dualBasis_eq_iff, dualBasis_flip_dualBasis, dualBasis_injective, dualBasis_involutive, dualBasis_repr_apply, ext_iff_of_isSymm, ext_of_isSymm, isAdjointPairLeftAdjointOfNondegenerate, isAdjointPair_iff_eq_of_nondegenerate, isAdjointPair_unique_of_nondegenerate, isAlt_neg, isAlt_zero, isNonneg_def, isNonneg_iff, isNonneg_zero, isPosSemidef_def, isPosSemidef_iff, isPosSemidef_zero, isRefl_neg, isRefl_zero, isSymm_def, isSymm_iff, isSymm_iff_basis, isSymm_iff_flip, isSymm_neg, isSymm_zero, nonDegenerateFlip_iff, nondegenerate_congr_iff, nondegenerate_flip_iff, not_nondegenerate_zero, symmCompOfNondegenerate_left_apply, toDual_def	69
Total	78

LinearMap.BilinForm

Definitions

Name	Category	Theorems
IsAlt 📖	MathDef	2 math math: isAlt_zero, isAlt_neg
IsNonneg 📖	CompData	5 math math: isNonneg_iff, isNonneg_def, IsPosSemidef.isNonneg, isPosSemidef_def, isNonneg_zero
IsPosSemidef 📖	CompData	7 math math: ProbabilityTheory.isGaussian_iff_gaussian_charFun, isPosSemidef_iff, ProbabilityTheory.isPosSemidef_covarianceBilin, isPosSemidef_def, ProbabilityTheory.isGaussian_iff_gaussian_charFunDual, ProbabilityTheory.isPosSemidef_covarianceBilinDual, isPosSemidef_zero
IsRefl 📖	MathDef	4 math math: IsAlt.isRefl, isRefl_zero, IsSymm.isRefl, isRefl_neg
IsSymm 📖	CompData	9 math math: isSymm_iff_flip, isSymm_iff, isPosSemidef_def, isSymm_neg, IsPosSemidef.isSymm, Algebra.traceForm_isSymm, isSymm_def, isSymm_zero, isSymm_iff_basis
dualBasis 📖	CompOp	13 math math: integralClosure_le_span_dualBasis, apply_dualBasis_left, dualSubmodule_span_of_basis, Module.Basis.traceDual_def, dualBasis_repr_apply, dualBasis_injective, dualBasis_eq_iff, dualBasis_dualBasis, IsIntegralClosure.range_le_span_dualBasis, dualBasis_involutive, dualBasis_dualBasis_flip, apply_dualBasis_right, dualBasis_flip_dualBasis
leftAdjointOfNondegenerate 📖	CompOp	2 math math: isAdjointPair_iff_eq_of_nondegenerate, isAdjointPairLeftAdjointOfNondegenerate
symmCompOfNondegenerate 📖	CompOp	2 math math: symmCompOfNondegenerate_left_apply, comp_symmCompOfNondegenerate_apply
toDual 📖	CompOp	2 math math: toDual_def, apply_toDual_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_dualBasis_left 📖	mathematical	Nondegenerate Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Module.Basis.instFunLike dualBasis AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Module.Basis.finiteDimensional_of_finite dualBasis.eq_1 RingHomInvPair.ids Module.Basis.map_apply smulCommClass_self Module.Basis.coe_dualBasis Algebra.to_smulCommClass toDual_def LinearEquiv.apply_symm_apply Module.Basis.coord_apply Module.Basis.repr_self Finsupp.single_apply
apply_dualBasis_right 📖	mathematical	Nondegenerate Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid IsSymm	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Module.Basis.instFunLike dualBasis AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	IsSymm.eq apply_dualBasis_left
apply_toDual_symm_apply 📖	mathematical	Nondegenerate Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHomInvPair.ids Module.Dual Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm toDual	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearEquiv.apply_symm_apply
compLeft_injective 📖	mathematical	Nondegenerate CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.BilinForm compLeft	—	LinearMap.ext eq_of_sub_eq_zero sub_left compLeft_apply sub_self
comp_symmCompOfNondegenerate_apply 📖	mathematical	Nondegenerate Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	DFunLike.coe LinearMap.BilinForm LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module DivisionSemiring.toSemiring Semifield.toDivisionSemiring symmCompOfNondegenerate	—	symmCompOfNondegenerate.eq_1 RingHomInvPair.ids Algebra.to_smulCommClass LinearEquiv.apply_symm_apply
dualBasis_dualBasis 📖	mathematical	Nondegenerate Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid IsSymm	dualBasis	—	Nondegenerate.flip RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass isSymm_iff_flip dualBasis_dualBasis_flip
dualBasis_dualBasis_flip 📖	mathematical	Nondegenerate Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	dualBasis flip Nondegenerate.flip	—	Module.Basis.eq_of_apply_eq Nondegenerate.flip LinearMap.ker_eq_bot Nondegenerate.ker_eq_bot Module.Basis.ext apply_dualBasis_left RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass
dualBasis_eq_iff 📖	mathematical	Nondegenerate Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	DFunLike.coe Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Module.Basis.instFunLike dualBasis LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	apply_dualBasis_left RingHomInvPair.ids Module.Basis.ext_elem_iff dualBasis_repr_apply
dualBasis_flip_dualBasis 📖	mathematical	Nondegenerate Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	dualBasis flip Nondegenerate.flip	—	dualBasis_dualBasis_flip Nondegenerate.flip
dualBasis_injective 📖	mathematical	Nondegenerate Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid IsSymm	Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring dualBasis	—	Function.Involutive.injective dualBasis_involutive
dualBasis_involutive 📖	mathematical	Nondegenerate Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid IsSymm	Function.Involutive Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring dualBasis	—	dualBasis_dualBasis
dualBasis_repr_apply 📖	mathematical	Nondegenerate Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr dualBasis LinearMap CommSemiring.toSemiring LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module Module.Basis Module.Basis.instFunLike	—	Module.Basis.finiteDimensional_of_finite RingHomInvPair.ids dualBasis.eq_1 Module.Basis.map_repr LinearEquiv.symm_symm LinearEquiv.trans_apply smulCommClass_self Module.Basis.dualBasis_repr Algebra.to_smulCommClass toDual_def
ext_iff_of_isSymm 📖	mathematical	IsSymm Semifield.toCommSemiring Field.toSemifield	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module	—	Nat.instAtLeastTwoHAddOfNat ext_of_isSymm
ext_of_isSymm 📖	—	IsSymm Semifield.toCommSemiring Field.toSemifield DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module	—	—	Nat.instAtLeastTwoHAddOfNat ext IsSymm.polarization
isAdjointPairLeftAdjointOfNondegenerate 📖	mathematical	Nondegenerate Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	LinearMap.IsAdjointPair NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule RingHom.id DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring LinearMap.instFunLike leftAdjointOfNondegenerate	—	symmCompOfNondegenerate_left_apply
isAdjointPair_iff_eq_of_nondegenerate 📖	mathematical	Nondegenerate Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	LinearMap.IsAdjointPair NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule RingHom.id DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring LinearMap.instFunLike leftAdjointOfNondegenerate	—	isAdjointPair_unique_of_nondegenerate isAdjointPairLeftAdjointOfNondegenerate
isAdjointPair_unique_of_nondegenerate 📖	—	Nondegenerate CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.IsAdjointPair NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule RingHom.id DFunLike.coe LinearMap LinearMap.instFunLike	—	—	compLeft_injective ext compLeft_apply
isAlt_neg 📖	mathematical	—	IsAlt CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.BilinForm LinearMap.instNeg LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommGroup Ring.toAddCommGroup CommRing.toRing LinearMap.module	—	IsAlt.neg neg_neg
isAlt_zero 📖	mathematical	—	IsAlt LinearMap.BilinForm LinearMap.instZero LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module	—	—
isNonneg_def 📖	mathematical	—	IsNonneg MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module	—	—
isNonneg_iff 📖	mathematical	—	IsNonneg LinearMap.IsNonneg RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	isNonneg_def Algebra.to_smulCommClass LinearMap.isNonneg_def
isNonneg_zero 📖	mathematical	—	IsNonneg Preorder.toLE LinearMap.BilinForm LinearMap.instZero LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module	—	isNonneg_iff LinearMap.isNonneg_zero
isPosSemidef_def 📖	mathematical	—	IsPosSemidef IsSymm IsNonneg	—	IsPosSemidef.isSymm IsPosSemidef.isNonneg
isPosSemidef_iff 📖	mathematical	—	IsPosSemidef LinearMap.IsPosSemidef RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	isPosSemidef_def Iff.and isSymm_iff isNonneg_iff LinearMap.isPosSemidef_def
isPosSemidef_zero 📖	mathematical	—	IsPosSemidef Preorder.toLE LinearMap.BilinForm LinearMap.instZero LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module	—	isPosSemidef_iff LinearMap.isPosSemidef_zero
isRefl_neg 📖	mathematical	—	IsRefl CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.BilinForm LinearMap.instNeg LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommGroup Ring.toAddCommGroup CommRing.toRing LinearMap.module	—	IsRefl.neg neg_neg
isRefl_zero 📖	mathematical	—	IsRefl LinearMap.BilinForm LinearMap.instZero LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module	—	—
isSymm_def 📖	mathematical	—	IsSymm DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module	—	—
isSymm_iff 📖	mathematical	—	IsSymm LinearMap.IsSymm RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Algebra.to_smulCommClass
isSymm_iff_basis 📖	mathematical	—	IsSymm DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module Module.Basis Module.Basis.instFunLike	—	Submodule.mem_span_iff_exists_finset_subset Module.Basis.span_eq Algebra.to_smulCommClass map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.coe_sum Finset.sum_apply Finset.mul_sum Finset.sum_comm mul_left_comm
isSymm_iff_flip 📖	mathematical	—	IsSymm DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm LinearMap.addCommMonoid LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv flipHom	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass ext flip_apply
isSymm_neg 📖	mathematical	—	IsSymm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.BilinForm LinearMap.instNeg LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommGroup Ring.toAddCommGroup CommRing.toRing LinearMap.module	—	IsSymm.neg neg_neg
isSymm_zero 📖	mathematical	—	IsSymm LinearMap.BilinForm LinearMap.instZero LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module	—	—
nonDegenerateFlip_iff 📖	mathematical	—	Nondegenerate flip	—	nondegenerate_flip_iff
nondegenerate_congr_iff 📖	mathematical	—	Nondegenerate DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm LinearMap.addCommMonoid LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv congr	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass RingHomCompTriple.ids congr_congr RingHomInvPair.triples₂ LinearEquiv.self_trans_symm congr_refl LinearEquiv.refl_apply Nondegenerate.congr
nondegenerate_flip_iff 📖	mathematical	—	Nondegenerate flip	—	Nondegenerate.flip
not_nondegenerate_zero 📖	mathematical	—	Nondegenerate LinearMap.BilinForm LinearMap.instZero LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module	—	exists_ne
symmCompOfNondegenerate_left_apply 📖	mathematical	Nondegenerate Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module DivisionSemiring.toSemiring Semifield.toDivisionSemiring symmCompOfNondegenerate	—	comp_symmCompOfNondegenerate_apply
toDual_def 📖	mathematical	Nondegenerate Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	DFunLike.coe Module.Dual DivisionSemiring.toSemiring Semifield.toDivisionSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearEquiv RingHomInvPair.ids LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass CommSemiring.toSemiring Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toDual LinearMap LinearMap.BilinForm	—	RingHomInvPair.ids Algebra.to_smulCommClass

LinearMap.BilinForm.IsAlt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	LinearMap.BilinForm.IsAlt	LinearMap.BilinForm LinearMap.instAdd LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module	—	add_zero
eq_of_add_add_eq_zero 📖	mathematical	LinearMap.BilinForm.IsAlt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module	—	LinearMap.IsAlt.eq_of_add_add_eq_zero
isRefl 📖	mathematical	LinearMap.BilinForm.IsAlt CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	LinearMap.BilinForm.IsRefl	—	LinearMap.IsAlt.isRefl
neg 📖	mathematical	LinearMap.BilinForm.IsAlt CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	LinearMap.BilinForm LinearMap.instNeg LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommGroup Ring.toAddCommGroup CommRing.toRing LinearMap.module	—	neg_eq_zero
neg_eq 📖	mathematical	LinearMap.BilinForm.IsAlt CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module	—	LinearMap.IsAlt.neg
self_eq_zero 📖	mathematical	LinearMap.BilinForm.IsAlt	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	LinearMap.IsAlt.self_eq_zero
smul 📖	mathematical	LinearMap.BilinForm.IsAlt	LinearMap.BilinForm LinearMap.instSMul LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid LinearMap.instDistribMulAction LinearMap.instSMulCommClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	smul_zero
sub 📖	mathematical	LinearMap.BilinForm.IsAlt CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	LinearMap.BilinForm LinearMap.instSub LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommGroup Ring.toAddCommGroup CommRing.toRing LinearMap.module	—	sub_zero

LinearMap.BilinForm.IsNonneg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	LinearMap.BilinForm.IsNonneg Preorder.toLE	LinearMap.BilinForm LinearMap.instAdd LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module	—	add_nonneg nonneg
nonneg 📖	mathematical	LinearMap.BilinForm.IsNonneg	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module	—	—
smul 📖	mathematical	LinearMap.BilinForm.IsNonneg Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	LinearMap.BilinForm LinearMap.instSMul LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule LinearMap.addCommMonoid LinearMap.module DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid LinearMap.instDistribMulAction Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass	—	Algebra.to_smulCommClass LinearMap.instSMulCommClass mul_nonneg nonneg

LinearMap.BilinForm.IsPosSemidef

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	LinearMap.BilinForm.IsPosSemidef Preorder.toLE	LinearMap.BilinForm LinearMap.instAdd LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module	—	LinearMap.BilinForm.isPosSemidef_iff LinearMap.IsPosSemidef.add
isNonneg 📖	mathematical	LinearMap.BilinForm.IsPosSemidef	LinearMap.BilinForm.IsNonneg	—	—
isSymm 📖	mathematical	LinearMap.BilinForm.IsPosSemidef	LinearMap.BilinForm.IsSymm	—	—
smul 📖	mathematical	LinearMap.BilinForm.IsPosSemidef Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	LinearMap.BilinForm LinearMap.instSMul LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule LinearMap.addCommMonoid LinearMap.module DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid LinearMap.instDistribMulAction Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass	—	Algebra.to_smulCommClass LinearMap.instSMulCommClass LinearMap.BilinForm.isPosSemidef_def LinearMap.BilinForm.IsSymm.smul isSymm LinearMap.BilinForm.IsNonneg.smul isNonneg

LinearMap.BilinForm.IsRefl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero 📖	—	LinearMap.BilinForm.IsRefl DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—	—
groupSMul 📖	mathematical	LinearMap.BilinForm.IsRefl	LinearMap.BilinForm LinearMap.instSMul LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommMonoid.toAddMonoid LinearMap.instDistribMulAction LinearMap.instSMulCommClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	LinearMap.instSMulCommClass smul_eq_zero_iff_eq
neg 📖	mathematical	LinearMap.BilinForm.IsRefl CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	LinearMap.BilinForm LinearMap.instNeg LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommGroup Ring.toAddCommGroup CommRing.toRing LinearMap.module	—	neg_eq_zero
smul 📖	mathematical	LinearMap.BilinForm.IsRefl	LinearMap.BilinForm LinearMap.instSMul LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid LinearMap.instDistribMulAction Module.toDistribMulAction LinearMap.instSMulCommClass	—	LinearMap.instSMulCommClass smul_eq_zero IsDomain.toIsCancelMulZero smul_eq_zero_of_left smul_eq_zero_of_right

LinearMap.BilinForm.IsSymm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	LinearMap.BilinForm.IsSymm	LinearMap.BilinForm LinearMap.instAdd LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module	—	eq
eq 📖	mathematical	LinearMap.BilinForm.IsSymm	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module	—	—
isRefl 📖	mathematical	LinearMap.BilinForm.IsSymm	LinearMap.BilinForm.IsRefl	—	eq
neg 📖	mathematical	LinearMap.BilinForm.IsSymm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	LinearMap.BilinForm LinearMap.instNeg LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommGroup Ring.toAddCommGroup CommRing.toRing LinearMap.module	—	eq
polarization 📖	mathematical	LinearMap.BilinForm.IsSymm Semifield.toCommSemiring Field.toSemifield	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.sub_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_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw 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.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.Ring.add_pf_add_zero Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.toProd_pf 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.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero mul_assoc inv_mul_cancel₀ two_ne_zero mul_one
restrict 📖	mathematical	LinearMap.BilinForm.IsSymm	Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module LinearMap.BilinForm.restrict	—	eq
smul 📖	mathematical	LinearMap.BilinForm.IsSymm	LinearMap.BilinForm LinearMap.instSMul LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid LinearMap.instDistribMulAction LinearMap.instSMulCommClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	LinearMap.instSMulCommClass eq
sub 📖	mathematical	LinearMap.BilinForm.IsSymm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	LinearMap.BilinForm LinearMap.instSub LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommGroup Ring.toAddCommGroup CommRing.toRing LinearMap.module	—	eq

LinearMap.BilinForm.Nondegenerate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
flip 📖	mathematical	LinearMap.BilinForm.Nondegenerate	LinearMap.BilinForm.flip	—	—
ker_eq_bot 📖	mathematical	LinearMap.BilinForm.Nondegenerate	LinearMap.ker LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module Bot.bot Submodule Submodule.instBot	—	smulCommClass_self LinearMap.separatingLeft_iff_ker_eq_bot
ne_zero 📖	—	LinearMap.BilinForm.Nondegenerate	—	—	LinearMap.BilinForm.not_nondegenerate_zero

---

← Back to Index