Documentation Verification Report

Signature

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

Statistics

Metric	Count
Definitions `sigNeg`, `sigPos`	2
Theorems `sigNeg_of_equiv_weightedSumSquares`, `sigNeg_weightedSumSquares`, `sigPos_add_finrank_le_of_nonpos`, `sigPos_add_sigNeg_add_radical`, `sigPos_of_equiv_weightedSumSquares`, `sigPos_weightedSumSquares`, `sigNeg_eq`, `sigPos_eq`, `map_negDef_iff`, `map_posDef_iff`, `exists_finrank_eq_sigNeg_and_negDef`, `exists_finrank_eq_sigPos_and_posDef`, `le_sigNeg_of_negDef`, `le_sigPos_of_posDef`, `sigNeg_isGreatest`, `sigNeg_neg`, `sigPos_isGreatest`, `sigPos_le_finrank`, `sigPos_neg`	19
Total	21

QuadraticForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sigNeg_of_equiv_weightedSumSquares` 📖	mathematical	—	`sigNeg` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Set.ncard` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Algebra.to_smulCommClass` `QuadraticMap.Equivalent.sigNeg_eq` `sigNeg_weightedSumSquares`
`sigNeg_weightedSumSquares` 📖	mathematical	—	`sigNeg` `Pi.addCommGroup` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Pi.Function.module` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `QuadraticMap.weightedSumSquares` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.to_smulCommClass` `Algebra.id` `Set.ncard` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Algebra.to_smulCommClass` `QuadraticMap.ext` `QuadraticMap.weightedSumSquares_apply` `Finset.sum_congr` `neg_mul` `Finset.sum_neg_distrib` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `sigPos_weightedSumSquares`
`sigPos_add_finrank_le_of_nonpos` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `QuadraticForm` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `QuadraticMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`sigPos` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.finrank` `Subspace` `Field.toDivisionRing` `SetLike.instMembership` `Submodule.setLike` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Semifield.toDivisionSemiring` `Field.toSemifield` `Submodule.addCommMonoid` `Submodule.module`	—	`exists_finrank_eq_sigPos_and_posDef` `IsNoetherianRing.strongRankCondition` `EuclideanDomain.toNontrivial` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `Submodule.finrank_add_finrank_le_of_disjoint` `le_bot_iff` `Submodule.eq_bot_iff`
`sigPos_add_sigNeg_add_radical` 📖	mathematical	—	`sigPos` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `sigNeg` `Module.finrank` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `QuadraticMap.radical` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Semiring.toModule` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module`	—	`Nat.instAtLeastTwoHAddOfNat` `CharZero.NeZero.two` `IsStrictOrderedRing.toCharZero` `Algebra.to_smulCommClass` `equivalent_weightedSumSquares` `QuadraticMap.Equivalent.sigPos_eq` `QuadraticMap.Equivalent.sigNeg_eq` `QuadraticMap.Equivalent.rank_radical_eq` `Nat.card_fin`
`sigPos_of_equiv_weightedSumSquares` 📖	mathematical	—	`sigPos` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Set.ncard` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Algebra.to_smulCommClass` `QuadraticMap.Equivalent.sigPos_eq` `sigPos_weightedSumSquares`
`sigPos_weightedSumSquares` 📖	mathematical	—	`sigPos` `Pi.addCommGroup` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Pi.Function.module` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `QuadraticMap.weightedSumSquares` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.to_smulCommClass` `Algebra.id` `Set.ncard` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Algebra.to_smulCommClass` `Set.ext` `Set.ncard_add_ncard_compl` `Set.toFinite` `Subtype.finite` `Finite.of_fintype` `sigPos_isGreatest` `FiniteDimensional.finiteDimensional_pi'` `FiniteDimensional.finiteDimensional_self` `IsNoetherianRing.strongRankCondition` `EuclideanDomain.toNontrivial` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `Pi.dim_spanSubset` `Nat.card_eq_fintype_card` `Module.finrank_fintype_fun_eq_card` `sigPos_add_finrank_le_of_nonpos`

QuadraticMap.Equivalent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sigNeg_eq` 📖	mathematical	—	`sigNeg`	—	`sigPos_eq` `RingHomInvPair.ids` `QuadraticMap.IsometryEquiv.map_app`
`sigPos_eq` 📖	mathematical	—	`sigPos`	—	`Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable` `Equiv.exists_congr` `RingHomSurjective.ids` `RingHomInvPair.ids` `Iff.and` `eq_iff_eq_cancel_right` `LinearEquiv.finrank_map_eq` `QuadraticMap.IsometryEquiv.map_posDef_iff` `LinearEquiv.finrank_eq`

QuadraticMap.IsometryEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_negDef_iff` 📖	mathematical	—	`QuadraticMap.PosDef` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.map` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `toLinearEquiv` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Submodule.addCommMonoid` `Submodule.module` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `QuadraticMap.restrict` `QuadraticForm` `QuadraticMap.instNeg` `Ring.toAddCommGroup` `CommRing.toRing`	—	`RingHomSurjective.ids` `RingHomInvPair.ids` `EquivLike.toEmbeddingLike` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `instLinearEquivClass` `map_app`
`map_posDef_iff` 📖	mathematical	—	`QuadraticMap.PosDef` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.map` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `toLinearEquiv` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Submodule.addCommMonoid` `Submodule.module` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `QuadraticMap.restrict`	—	`RingHomSurjective.ids` `RingHomInvPair.ids` `EquivLike.toEmbeddingLike` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `instLinearEquivClass` `map_app`

(root)

Definitions

Name	Category	Theorems
`sigNeg` 📖	CompOp	9 math math: `sigNeg_isGreatest`, `QuadraticMap.Equivalent.sigNeg_eq`, `sigNeg_neg`, `QuadraticForm.sigPos_add_sigNeg_add_radical`, `exists_finrank_eq_sigNeg_and_negDef`, `sigPos_neg`, `QuadraticForm.sigNeg_weightedSumSquares`, `le_sigNeg_of_negDef`, `QuadraticForm.sigNeg_of_equiv_weightedSumSquares`
`sigPos` 📖	CompOp	11 math math: `exists_finrank_eq_sigPos_and_posDef`, `QuadraticMap.Equivalent.sigPos_eq`, `sigPos_isGreatest`, `sigNeg_neg`, `le_sigPos_of_posDef`, `QuadraticForm.sigPos_add_sigNeg_add_radical`, `sigPos_le_finrank`, `sigPos_neg`, `QuadraticForm.sigPos_of_equiv_weightedSumSquares`, `QuadraticForm.sigPos_weightedSumSquares`, `QuadraticForm.sigPos_add_finrank_le_of_nonpos`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_finrank_eq_sigNeg_and_negDef` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Module.finrank` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `sigNeg` `QuadraticMap.PosDef` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `QuadraticMap.restrict` `QuadraticForm` `QuadraticMap.instNeg` `Ring.toAddCommGroup` `CommRing.toRing`	—	`exists_finrank_eq_sigPos_and_posDef`
`exists_finrank_eq_sigPos_and_posDef` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Module.finrank` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `sigPos` `QuadraticMap.PosDef` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `QuadraticMap.restrict`	—	`sigPos_isGreatest`
`le_sigNeg_of_negDef` 📖	mathematical	`QuadraticMap.PosDef` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `QuadraticMap.restrict` `QuadraticForm` `QuadraticMap.instNeg` `Ring.toAddCommGroup` `CommRing.toRing`	`Module.finrank` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `sigNeg`	—	`le_sigPos_of_posDef`
`le_sigPos_of_posDef` 📖	mathematical	`QuadraticMap.PosDef` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `QuadraticMap.restrict`	`Module.finrank` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `sigPos`	—	`sigPos_isGreatest`
`sigNeg_isGreatest` 📖	mathematical	—	`IsGreatest` `setOf` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Module.finrank` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `QuadraticMap.PosDef` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `QuadraticMap.restrict` `QuadraticForm` `QuadraticMap.instNeg` `Ring.toAddCommGroup` `CommRing.toRing` `sigNeg`	—	`sigPos_isGreatest`
`sigNeg_neg` 📖	mathematical	—	`sigNeg` `QuadraticForm` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `QuadraticMap.instNeg` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `sigPos`	—	`sigPos_neg` `neg_neg`
`sigPos_isGreatest` 📖	mathematical	—	`IsGreatest` `setOf` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Module.finrank` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `QuadraticMap.PosDef` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `QuadraticMap.restrict` `sigPos`	—	`Finset.mem_filter` `Finset.max'_mem` `Finset.le_max'` `Finset.mem_Iic` `Submodule.finrank_le`
`sigPos_le_finrank` 📖	mathematical	—	`sigPos` `Module.finrank` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`Finset.mem_Iic` `Finset.mem_of_mem_filter` `Finset.max'_mem`
`sigPos_neg` 📖	mathematical	—	`sigPos` `QuadraticForm` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `QuadraticMap.instNeg` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `sigNeg`	—	—

---

← Back to Index