Dual

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

Statistics

Metric	Count
Definitions Dual, dualProd, dualProd, dualProdIsometry, dualProdProdIsometry, toDualProd	6
Theorems linearIndependent_of_pairwise_le_zero, toQuadraticForm, dualProd_apply_apply, isSymm_dualProd, separatingLeft_dualProd, dualProdIsometry_invFun, dualProdIsometry_toFun, dualProdProdIsometry_invFun, dualProdProdIsometry_toFun, dualProd_apply, toDualProd_apply	11
Total	17

Configuration

Definitions

Name	Category	Theorems
Dual 📖	CompOp	3 math math: Dual.Nondegenerate, instFiniteDual, ProjectivePlane.Dual.order

LinearMap

Definitions

Name	Category	Theorems
dualProd 📖	CompOp	4 math math: isSymm_dualProd, dualProd_apply_apply, dualProd.toQuadraticForm, separatingLeft_dualProd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dualProd_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual Prod.instAddCommMonoid addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Prod.instModule module instFunLike Algebra.to_smulCommClass Algebra.id dualProd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Algebra.to_smulCommClass
isSymm_dualProd 📖	mathematical	—	IsSymm Module.Dual CommSemiring.toSemiring Prod.instAddCommMonoid addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id Prod.instModule module Algebra.to_smulCommClass Algebra.id dualProd	—	Algebra.to_smulCommClass add_comm
separatingLeft_dualProd 📖	mathematical	—	SeparatingLeft Module.Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Prod.instAddCommMonoid addCommMonoid RingHom.id Prod.instModule module Algebra.to_smulCommClass Algebra.id dualProd smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction DFunLike.coe LinearMap instFunLike Module.Dual.eval	—	Algebra.to_smulCommClass smulCommClass_self separatingLeft_iff_ker_eq_bot ker_eq_bot RingHomInvPair.ids RingHomCompTriple.ids Function.Injective.of_comp_iff LinearEquiv.injective LinearEquiv.coe_toLinearMap coe_comp ext zero_add map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass add_zero coe_prodMap Prod.map_injective Zero.instNonempty

LinearMap.BilinForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linearIndependent_of_pairwise_le_zero 📖	mathematical	QuadraticMap.PosDef CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule LinearMap.BilinMap.toQuadraticMap Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe Module.Dual LinearMap.instFunLike RingHom.id Pairwise Preorder.toLE LinearMap LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module	LinearIndependent	—	linearIndependent_iff' Finset.sum_congr neg_smul Finset.sum_neg_distrib Finset.sum_union Finset.sum_subset Finset.filter.congr_simp IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing zero_smul Finset.sum_nonneg Algebra.to_smulCommClass map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass map_neg LinearMap.coe_sum Finset.sum_apply Finset.mul_sum QuadraticMap.PosDef.le_zero_iff map_zero AddMonoidHomClass.toZeroHomClass mul_pos IsStrictOrderedRing.toPosMulStrictMono Finset.sum_eq_zero_iff_of_nonneg

LinearMap.dualProd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toQuadraticForm 📖	mathematical	—	LinearMap.BilinMap.toQuadraticMap Module.Dual CommSemiring.toSemiring Prod.instAddCommMonoid LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id Prod.instModule LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.dualProd QuadraticForm QuadraticMap AddMonoid.toNatSMul AddCommMonoid.toAddMonoid QuadraticMap.instAddCommMonoid QuadraticForm.dualProd	—	QuadraticMap.ext Algebra.to_smulCommClass two_nsmul

QuadraticForm

Definitions

Name	Category	Theorems
dualProd 📖	CompOp	7 math math: dualProd_apply, dualProdIsometry_invFun, dualProdIsometry_toFun, toDualProd_apply, dualProdProdIsometry_toFun, LinearMap.dualProd.toQuadraticForm, dualProdProdIsometry_invFun
dualProdIsometry 📖	CompOp	2 math math: dualProdIsometry_invFun, dualProdIsometry_toFun
dualProdProdIsometry 📖	CompOp	2 math math: dualProdProdIsometry_toFun, dualProdProdIsometry_invFun
toDualProd 📖	CompOp	1 math math: toDualProd_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dualProdIsometry_invFun 📖	mathematical	—	LinearEquiv.invFun CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.Dual Prod.instAddCommMonoid LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Prod.instModule LinearMap.module Algebra.to_smulCommClass Algebra.id QuadraticMap.IsometryEquiv.toLinearEquiv dualProd dualProdIsometry DFunLike.coe AddEquiv Prod.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm AddEquiv.prodCongr LinearEquiv.toAddEquiv LinearEquiv.dualMap LinearEquiv.symm	—	RingHomInvPair.ids Algebra.to_smulCommClass
dualProdIsometry_toFun 📖	mathematical	—	DFunLike.coe QuadraticMap.IsometryEquiv Module.Dual CommSemiring.toSemiring Prod.instAddCommMonoid LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id Prod.instModule LinearMap.module Algebra.to_smulCommClass Algebra.id dualProd EquivLike.toFunLike QuadraticMap.IsometryEquiv.instEquivLike dualProdIsometry AddEquiv Prod.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddEquiv.instEquivLike AddEquiv.prodCongr LinearEquiv.toAddEquiv RingHomInvPair.ids LinearEquiv.dualMap LinearEquiv.symm	—	RingHomInvPair.ids Algebra.to_smulCommClass
dualProdProdIsometry_invFun 📖	mathematical	—	LinearEquiv.invFun CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.Dual Prod.instAddCommMonoid Prod.instModule LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id QuadraticMap.IsometryEquiv.toLinearEquiv dualProd QuadraticMap.prod dualProdProdIsometry DFunLike.coe LinearEquiv EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm LinearEquiv.prodCongr Module.dualProdDualEquivDual LinearEquiv.refl	—	RingHomInvPair.ids Algebra.to_smulCommClass
dualProdProdIsometry_toFun 📖	mathematical	—	DFunLike.coe QuadraticMap.IsometryEquiv Module.Dual CommSemiring.toSemiring Prod.instAddCommMonoid Prod.instModule LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module Algebra.to_smulCommClass Algebra.id dualProd QuadraticMap.prod EquivLike.toFunLike QuadraticMap.IsometryEquiv.instEquivLike dualProdProdIsometry LinearMap.comp LinearMap.inl LinearMap.inr	—	Algebra.to_smulCommClass
dualProd_apply 📖	mathematical	—	DFunLike.coe QuadraticMap Module.Dual CommSemiring.toSemiring Prod.instAddCommMonoid LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id Prod.instModule LinearMap.module Algebra.to_smulCommClass Algebra.id QuadraticMap.instFunLike dualProd LinearMap.instFunLike	—	Algebra.to_smulCommClass
toDualProd_apply 📖	mathematical	—	DFunLike.coe QuadraticMap.Isometry Module.Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Prod.instAddCommMonoid LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id Prod.instModule LinearMap.module Algebra.to_smulCommClass Algebra.id QuadraticMap.prod QuadraticForm QuadraticMap.instNeg Ring.toAddCommGroup CommRing.toRing dualProd QuadraticMap.Isometry.instFunLike toDualProd LinearMap AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.instFunLike QuadraticMap LinearMap.BilinMap QuadraticMap.instAddCommMonoid QuadraticMap.instModuleOfSMulCommClass QuadraticMap.associated QuadraticMap.instInvertibleEndOfNat SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	Nat.instAtLeastTwoHAddOfNat Algebra.to_smulCommClass

---

← Back to Index