Real

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

Statistics

Metric	Count
Definitions isometryEquivSignWeightedSumSquares	1
Theorems equivalent_one_neg_one_weighted_sum_squared, equivalent_one_zero_neg_one_weighted_sum_squared, equivalent_signType_weighted_sum_squared, equivalent_sign_ne_zero_weighted_sum_squared	4
Total	5

QuadraticForm

Definitions

Name	Category	Theorems
isometryEquivSignWeightedSumSquares 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivalent_one_neg_one_weighted_sum_squared 📖	mathematical	LinearMap.SeparatingLeft Real Real.instCommSemiring AddCommGroup.toAddCommMonoid Real.instAddCommGroup Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring CommRing.toCommSemiring Real.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 Real.instField RCLike.charZero_rclike Real.instRCLike	Real.instNeg Real.instOne QuadraticMap.Equivalent Pi.addCommMonoid Module.finrank Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module QuadraticMap.weightedSumSquares Fin.fintype Real.instMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Algebra.to_smulCommClass Algebra.id	—	smulCommClass_self LinearMap.instSMulCommClass RCLike.charZero_rclike Algebra.to_smulCommClass equivalent_sign_ne_zero_weighted_sum_squared SignType.coe_neg
equivalent_one_zero_neg_one_weighted_sum_squared 📖	mathematical	—	Real Real.instNeg Real.instOne Real.instZero QuadraticMap.Equivalent Real.instCommSemiring AddCommGroup.toAddCommMonoid Pi.addCommMonoid Module.finrank Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule QuadraticMap.weightedSumSquares Fin.fintype Real.instMonoid Module.toDistribMulAction Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Algebra.to_smulCommClass Algebra.id	—	Algebra.to_smulCommClass equivalent_signType_weighted_sum_squared NeZero.charZero_one RCLike.charZero_rclike SignType.coe_neg
equivalent_signType_weighted_sum_squared 📖	mathematical	—	QuadraticMap.Equivalent Real Real.instCommSemiring AddCommGroup.toAddCommMonoid Pi.addCommMonoid Module.finrank Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule QuadraticMap.weightedSumSquares Fin.fintype Real.instMonoid Module.toDistribMulAction Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Algebra.to_smulCommClass Algebra.id SignType.cast Real.instZero Real.instOne Real.instNeg	—	Algebra.to_smulCommClass equivalent_weightedSumSquares RCLike.charZero_rclike
equivalent_sign_ne_zero_weighted_sum_squared 📖	mathematical	LinearMap.SeparatingLeft Real Real.instCommSemiring AddCommGroup.toAddCommMonoid Real.instAddCommGroup Semiring.toModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring CommRing.toCommSemiring Real.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 Real.instField RCLike.charZero_rclike Real.instRCLike	QuadraticMap.Equivalent Pi.addCommMonoid Module.finrank Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module QuadraticMap.weightedSumSquares Fin.fintype Real.instMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Algebra.to_smulCommClass Algebra.id SignType.cast Real.instZero Real.instOne Real.instNeg	—	smulCommClass_self LinearMap.instSMulCommClass RCLike.charZero_rclike Units.smulCommClass_left Algebra.to_smulCommClass equivalent_weightedSumSquares_units_of_nondegenerate' sign_ne_zero Units.ne_zero Real.instNontrivial

---

← Back to Index