Complex

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

Statistics

Metric	Count
Definitions	0
Theorems complex_equivalent, equivalent_sum_squares	2
Total	2

QuadraticForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
complex_equivalent 📖	mathematical	LinearMap.SeparatingLeft Complex Complex.instCommSemiring AddCommGroup.toAddCommMonoid Complex.addCommGroup Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring CommRing.toCommSemiring Complex.commRing 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 invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Complex.instField Complex.instCharZero	QuadraticMap.Equivalent Complex Complex.instCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule	—	smulCommClass_self LinearMap.instSMulCommClass Complex.instCharZero equivalent_of_isAlgClosed Complex.isAlgClosed
equivalent_sum_squares 📖	mathematical	LinearMap.SeparatingLeft Complex Complex.instCommSemiring AddCommGroup.toAddCommMonoid Complex.addCommGroup Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring CommRing.toCommSemiring Complex.commRing 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 invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Complex.instField Complex.instCharZero	QuadraticMap.Equivalent Complex Complex.instCommSemiring AddCommGroup.toAddCommMonoid Pi.addCommMonoid Module.finrank Complex.instSemiring 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 Complex.commRing Algebra.to_smulCommClass Algebra.id Pi.instOne Complex.instOne	—	smulCommClass_self LinearMap.instSMulCommClass Complex.instCharZero equivalent_weightedSumSquares_of_isAlgClosed Complex.isAlgClosed

---

← Back to Index