Documentation Verification Report

SumsOfSquares

📁 Source: Mathlib/Algebra/Ring/SumsOfSquares.lean

Statistics

Metric	Count
Definitions `sumSq`, `IsSumSq`, `sumSq`, `sumSq`	4
Theorems `closure_isSquare`, `coe_sumSq`, `mem_sumSq`, `isSumSq`, `add`, `mul`, `mul_self`, `natCast`, `nonneg`, `one`, `prod`, `rec'`, `sum`, `sum_isSquare`, `sum_mul_self`, `sum_sq`, `isSumSq`, `closure_isSquare`, `coe_sumSq`, `mem_sumSq`, `sumSq_toAddSubmonoid`, `closure_isSquare`, `coe_sumSq`, `mem_sumSq`, `sumSq_toNonUnitalSubsemiring`, `isSumSq_iff`	26
Total	30

AddSubmonoid

Definitions

Name	Category	Theorems
`sumSq` 📖	CompOp	4 math math: `NonUnitalSubsemiring.sumSq_toAddSubmonoid`, `closure_isSquare`, `mem_sumSq`, `coe_sumSq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_isSquare` 📖	mathematical	—	`closure` `AddMonoid.toAddZeroClass` `setOf` `IsSquare` `sumSq`	—	`closure_eq_of_le` `IsSquare.isSumSq` `AddSubmonoidClass.toZeroMemClass` `instAddSubmonoidClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `mem_closure_of_mem`
`coe_sumSq` 📖	mathematical	—	`SetLike.coe` `AddSubmonoid` `AddMonoid.toAddZeroClass` `instSetLike` `sumSq` `setOf` `IsSumSq` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero`	—	—
`mem_sumSq` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `sumSq` `IsSumSq` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero`	—	—

IsSquare

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSumSq` 📖	mathematical	`IsSquare`	`IsSumSq` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddZero.toZero`	—	`exists_mul_self`

IsSumSq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	—	`IsSumSq` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—	`zero_add` `add_assoc`
`mul` 📖	—	`IsSumSq` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `Distrib.toAdd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—	`MulMemClass.mul_mem` `NonUnitalSubsemiringClass.mulMemClass` `NonUnitalSubsemiring.instNonUnitalSubsemiringClass`
`mul_self` 📖	mathematical	—	`IsSumSq` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddZero.toZero`	—	`add_zero`
`natCast` 📖	mathematical	—	`IsSumSq` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Nat.cast_zero` `Nat.cast_add` `Nat.cast_one` `add`
`nonneg` 📖	mathematical	`IsSumSq` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`rec'` `add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsSquare.nonneg` `IsOrderedRing.toPosMulMono`
`one` 📖	mathematical	—	`IsSumSq` `MulOne.toMul` `MulOneClass.toMulOne` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddZero.toZero` `MulOne.toOne`	—	`IsSquare.isSumSq`
`prod` 📖	mathematical	`IsSumSq` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toAdd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`Finset.prod` `CommSemiring.toCommMonoid`	—	`prod_mem` `SubsemiringClass.toSubmonoidClass` `Subsemiring.instSubsemiringClass`
`rec'` 📖	—	`zero` `IsSumSq`	—	—	`IsSquare.mul_self`
`sum` 📖	mathematical	`IsSumSq` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Finset.sum`	—	`sum_mem` `AddSubmonoid.instAddSubmonoidClass`
`sum_isSquare` 📖	mathematical	`IsSquare`	`IsSumSq` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset.sum`	—	`sum` `IsSquare.isSumSq`
`sum_mul_self` 📖	mathematical	—	`IsSumSq` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset.sum`	—	`sum`
`sum_sq` 📖	mathematical	—	`IsSumSq` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toAdd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`sum` `IsSquare.isSumSq` `IsSquare.sq`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSumSq` 📖	mathematical	—	`IsSumSq` `MulZeroClass.toZero` `instMulZeroClass`	—	`IsSumSq.natCast`

NonUnitalSubsemiring

Definitions

Name	Category	Theorems
`sumSq` 📖	CompOp	5 math math: `sumSq_toAddSubmonoid`, `Subsemiring.sumSq_toNonUnitalSubsemiring`, `mem_sumSq`, `coe_sumSq`, `closure_isSquare`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_isSquare` 📖	mathematical	—	`closure` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `setOf` `IsSquare` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `sumSq`	—	`Subsemigroup.nonUnitalSubsemiringClosure_eq_closure`
`coe_sumSq` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubsemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `instSetLike` `sumSq` `setOf` `IsSumSq` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toAdd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Set.ext`
`mem_sumSq` 📖	mathematical	—	`NonUnitalSubsemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `SetLike.instMembership` `instSetLike` `sumSq` `IsSumSq` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toAdd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`sumSq_toAddSubmonoid`
`sumSq_toAddSubmonoid` 📖	mathematical	—	`toAddSubmonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `sumSq` `AddSubmonoid.sumSq` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—

Subsemiring

Definitions

Name	Category	Theorems
`sumSq` 📖	CompOp	4 math math: `mem_sumSq`, `closure_isSquare`, `sumSq_toNonUnitalSubsemiring`, `coe_sumSq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_isSquare` 📖	mathematical	—	`closure` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `setOf` `IsSquare` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `sumSq`	—	`toNonUnitalSubsemiring_injective` `Submonoid.subsemiringClosure_toNonUnitalSubsemiring` `NonUnitalSubsemiring.closure_isSquare`
`coe_sumSq` 📖	mathematical	—	`SetLike.coe` `Subsemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSetLike` `sumSq` `setOf` `IsSumSq` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Set.ext`
`mem_sumSq` 📖	mathematical	—	`Subsemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `instSetLike` `sumSq` `IsSumSq` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`sumSq_toNonUnitalSubsemiring` 📖	mathematical	—	`toNonUnitalSubsemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `sumSq` `NonUnitalSubsemiring.sumSq` `CommSemiring.toNonUnitalCommSemiring`	—	—

(root)

Definitions

Name	Category	Theorems
`IsSumSq` 📖	CompData	18 math math: `Subsemiring.mem_sumSq`, `IsSumSq.one`, `isSemireal_iff_not_isSumSq_neg_one`, `IsSumSq.natCast`, `NonUnitalSubsemiring.mem_sumSq`, `Nat.isSumSq`, `AddSubmonoid.mem_sumSq`, `IsSquare.isSumSq`, `IsSumSq.sum_mul_self`, `Subsemiring.coe_sumSq`, `NonUnitalSubsemiring.coe_sumSq`, `RootPairing.rootForm_self_sum_of_squares`, `IsSumSq.sum_sq`, `AddSubmonoid.coe_sumSq`, `IsSumSq.sum_isSquare`, `isSumSq_iff`, `IsSumSq.mul_self`, `IsSemireal.not_isSumSq_neg_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSumSq_iff` 📖	mathematical	—	`IsSumSq`	—	—

---

← Back to Index