AlgClosed

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

Statistics

Metric	Count
Definitions isometryEquivSumSquares, isometryEquivSumSquaresUnits	2
Theorems equivalent_of_isAlgClosed, equivalent_weightedSumSquares_of_isAlgClosed	2
Total	4

QuadraticForm

Definitions

Name	Category	Theorems
isometryEquivSumSquares 📖	CompOp	—
isometryEquivSumSquaresUnits 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivalent_of_isAlgClosed 📖	mathematical	LinearMap.SeparatingLeft Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe LinearMap QuadraticMap LinearMap.BilinMap QuadraticMap.instAddCommMonoid LinearMap.addCommMonoid LinearMap.module QuadraticMap.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 QuadraticMap.associated QuadraticMap.instInvertibleEndOfNat	QuadraticMap.Equivalent Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule	—	Nat.instAtLeastTwoHAddOfNat smulCommClass_self LinearMap.instSMulCommClass QuadraticMap.Equivalent.trans Algebra.to_smulCommClass equivalent_weightedSumSquares_of_isAlgClosed QuadraticMap.Equivalent.symm
equivalent_weightedSumSquares_of_isAlgClosed 📖	mathematical	LinearMap.SeparatingLeft Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe LinearMap QuadraticMap LinearMap.BilinMap QuadraticMap.instAddCommMonoid LinearMap.addCommMonoid LinearMap.module QuadraticMap.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 QuadraticMap.associated QuadraticMap.instInvertibleEndOfNat	QuadraticMap.Equivalent Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid Pi.addCommMonoid Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule QuadraticMap.weightedSumSquares Fin.fintype MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.to_smulCommClass Algebra.id Pi.instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	Nat.instAtLeastTwoHAddOfNat smulCommClass_self LinearMap.instSMulCommClass Units.smulCommClass_left Algebra.to_smulCommClass equivalent_weightedSumSquares_units_of_nondegenerate'

---

← Back to Index