Documentation Verification Report

SumFourSquares

📁 Source: Mathlib/NumberTheory/SumFourSquares.lean

Statistics

Metric	Count
Definitions	0
Theorems `exists_sq_add_sq_add_one_eq_mul`, `lt_of_sum_four_squares_eq_mul`, `sq_add_sq_of_two_mul_sq_add_sq`, `sum_four_squares`, `euler_four_squares`, `sum_four_squares`, `euler_four_squares`	7
Total	7

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_sq_add_sq_add_one_eq_mul` 📖	mathematical	—	`Monoid.toNatPow` `Nat.instMonoid`	—	`Nat.Prime.eq_two_or_odd'` `Fact.out` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `one_pow` `zero_pow` `add_zero` `one_mul` `Nat.sq_add_sq_zmodEq` `modEq_iff_dvd` `ModEq.symm` `pos_of_mul_pos_left` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `instIsStrictOrderedRing` `mul_comm` `sub_neg_eq_add` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `instAddLeftMono` `add_nonneg` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `AddGroup.existsAddOfLE` `even_two_mul` `Mathlib.Meta.Positivity.pos_of_isNat` `instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_nonneg` `CanLift.prf` `instCanLiftIntNatCastLeOfNat` `LT.lt.le` `Nat.cast_pos` `Nat.cast_one` `instCharZero` `lt_of_sum_four_squares_eq_mul` `LE.le.trans_lt` `mul_le_mul'` `Nat.instMulLeftMono` `covariant_swap_mul_of_covariant_mul` `le_rfl` `Odd.not_two_dvd_nat` `lt_of_le_of_ne` `Nat.Prime.two_le` `Odd.ne_two_of_dvd_nat` `dvd_refl` `Nat.Prime.pos`
`lt_of_sum_four_squares_eq_mul` 📖	—	`Monoid.toNatPow` `Nat.instMonoid`	—	—	`lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `Mathlib.Tactic.Linarith.mul_neg` `neg_neg_of_pos` `instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `instCharZero` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Linarith.natCast_nonneg` `Mathlib.Tactic.Linarith.mul_eq` `neg_eq_zero` `sub_eq_zero_of_eq` `Nat.cast_add` `Nat.cast_pow` `Nat.cast_mul` `mul_nonneg_of_nonpos_of_nonpos` `AddGroup.existsAddOfLE` `IsOrderedRing.toMulPosMono` `covariant_swap_add_of_covariant_add` `instAddLeftMono` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le`
`sq_add_sq_of_two_mul_sq_add_sq` 📖	—	`Monoid.toNatPow` `instMonoid`	—	—	`Distrib.rightDistribClass` `Nat.instAtLeastTwoHAddOfNat` `mul_right_injective₀` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `mul_assoc` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.pow_nat` `Mathlib.Tactic.Ring.coeff_one` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.pow_bit0` `Mathlib.Tactic.Ring.pow_one` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `sq` `Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `instIsStrictOrderedRing` `neg_neg_of_pos` `instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`euler_four_squares` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid`	—	`cast_add` `cast_pow` `Int.natCast_natAbs` `cast_mul` `sq_abs` `euler_four_squares`
`sum_four_squares` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid`	—	`Prime.sum_four_squares` `euler_four_squares`

Nat.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_four_squares` 📖	mathematical	`Nat.Prime`	`Monoid.toNatPow` `Nat.instMonoid`	—	`Int.instCharZero` `Nat.cast_add` `Nat.cast_pow` `Int.natCast_natAbs` `sq_abs` `Int.exists_sq_add_sq_add_one_eq_mul` `one_pow` `zero_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `add_zero` `LE.le.eq_or_lt` `LT.lt.ne'` `one_mul` `two_mul` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `mul_pos_iff_of_pos_left` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `two_pos` `Nat.instZeroLEOneClass` `mul_assoc` `Nat.cast_mul` `LT.lt.trans` `LE.le.trans_lt` `mul_le_mul'` `Nat.instMulLeftMono` `covariant_swap_mul_of_covariant_mul` `le_rfl` `ZMod.natAbs_valMinAbs_le` `ZMod.coe_valMinAbs` `Int.cast_add` `Int.cast_pow` `Nat.cast_zero` `CharP.cast_eq_zero` `ZMod.charP` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `Int.cast_zero` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `eq_one_or_self_of_dvd` `mul_dvd_mul_iff_left` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero` `LT.lt.ne` `Int.lt_of_sum_four_squares_eq_mul` `mul_comm` `mul_neg` `sub_neg_eq_add` `Int.cast_sub` `Int.cast_mul` `Int.cast_natCast` `sub_self` `zero_sub` `neg_add_cancel` `add_comm` `add_assoc` `neg_mul` `add_left_comm` `sq` `sub_add_cancel` `Int.cast_neg` `add_neg_cancel` `add_sub_cancel_left` `mul_left_cancel₀` `Int.instIsCancelMulZero` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Int.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Nat.cast_ne_zero` `mul_mul_mul_comm` `mul_add` `Distrib.leftDistribClass`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`euler_four_squares` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Distrib.toMul`	—	`Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_nat` `Mathlib.Tactic.Ring.coeff_one` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.pow_bit0` `Mathlib.Tactic.Ring.pow_one` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow`

---

← Back to Index