Complex

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

Statistics

Metric	Count
Definitions isometryEquivSumSquares, isometryEquivSumSquaresUnits	2
Theorems complex_equivalent, equivalent_sum_squares	2
Total	4

QuadraticForm

Definitions

Name	Category	Theorems
isometryEquivSumSquares 📖	CompOp	—
isometryEquivSumSquaresUnits 📖	CompOp	—

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 NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring	—	smulCommClass_self LinearMap.instSMulCommClass Complex.instCharZero QuadraticMap.Equivalent.trans Algebra.to_smulCommClass equivalent_sum_squares QuadraticMap.Equivalent.symm
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 Pi.addCommMonoid Module.finrank Complex.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module QuadraticMap.weightedSumSquares Fin.fintype ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instModuleSelf Algebra.to_smulCommClass Algebra.id Pi.instOne Complex.instOne	—	smulCommClass_self LinearMap.instSMulCommClass Complex.instCharZero Units.smulCommClass_left Algebra.to_smulCommClass equivalent_weightedSumSquares_units_of_nondegenerate'

---

← Back to Index