Documentation Verification Report

NegOnePow

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

Statistics

Metric	Count
Definitions `negOnePow`	1
Theorems `abs_negOnePow`, `cast_negOnePow_natCast`, `coe_negOnePow_natCast`, `negOnePow_abs`, `negOnePow_add`, `negOnePow_def`, `negOnePow_eq_iff`, `negOnePow_eq_neg_one_iff`, `negOnePow_eq_one_iff`, `negOnePow_even`, `negOnePow_mul_self`, `negOnePow_neg`, `negOnePow_odd`, `negOnePow_one`, `negOnePow_sub`, `negOnePow_succ`, `negOnePow_two_mul`, `negOnePow_two_mul_add_one`, `negOnePow_zero`	19
Total	20

Int

Definitions

Name	Category	Theorems
`negOnePow` 📖	CompOp	101 math math: `Polynomial.ascPochhammer_smeval_neg_eq_descPochhammer`, `Polynomial.Chebyshev.U_eval_zero`, `negOnePow_abs`, `Function.Antiperiodic.add_int_mul_eq`, `CochainComplex.HomComplex.Cochain.δ_single`, `CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₁`, `CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃`, `CategoryTheory.Pretriangulated.Triangle.shiftFunctor_obj`, `HomologicalComplex₂.D₂_totalShift₁XIso_hom_assoc`, `HomologicalComplex₂.D₂_totalShift₂XIso_hom_assoc`, `Polynomial.Chebyshev.T_eval_zero`, `negOnePow_eq_neg_one_iff`, `Function.Antiperiodic.sub_int_mul_eq`, `negOnePow_eq_iff`, `CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_assoc`, `CochainComplex.HomComplex.δ_v`, `Polynomial.Chebyshev.T_eval_two_mul_zero`, `Polynomial.Chebyshev.T_eval_neg`, `ComplexShape.eulerCharSignsUpInt_χ`, `Ring.choose_neg`, `HomologicalComplex₂.ι_totalShift₂Iso_inv_f_assoc`, `CochainComplex.HomComplex.Cochain.leftShift_comp`, `Polynomial.Chebyshev.U_eval_neg_one`, `negOnePow_two_mul`, `cast_negOnePow`, `CochainComplex.HomComplex.Cochain.leftShift_rightShift_eq_negOnePow_rightShift_leftShift`, `CochainComplex.HomComplex.Cochain.leftShift_rightShift`, `negOnePow_add`, `CochainComplex.shiftShortComplexFunctor'_hom_app_τ₁`, `CochainComplex.HomComplex.Cochain.leftUnshift_v`, `CochainComplex.HomComplex.Cochain.rightShift_leftShift`, `HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom`, `negOnePow_neg`, `HomologicalComplex₂.D₁_totalShift₂XIso_hom_assoc`, `Function.Antiperiodic.add_zsmul_eq`, `negOnePow_one`, `HomologicalComplex₂.D₁_totalShift₁XIso_hom_assoc`, `CochainComplex.HomComplex.δ_comp`, `negOnePow_odd`, `ComplexShape.eulerCharSignsDownInt_χ`, `negOnePow_def`, `Ring.choose_neg'`, `CochainComplex.shiftFunctor_map_f`, `Function.Antiperiodic.zsmul_sub_eq`, `HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc`, `CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁`, `abs_negOnePow`, `negOnePow_two_mul_add_one`, `Polynomial.Chebyshev.U_eval_two_mul_zero`, `CochainComplex.ι_mapBifunctorShift₂Iso_hom_f`, `HomologicalComplex₂.D₁_totalShift₁XIso_hom`, `HomologicalComplex₂.D₂_totalShift₁XIso_hom`, `Matrix.submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det'`, `CochainComplex.HomComplex.Cochain.δ_toSingleMk`, `negOnePow_sub`, `Polynomial.Chebyshev.U_eval_neg`, `CochainComplex.HomComplex.Cochain.δ_shift`, `CochainComplex.shiftShortComplexFunctor'_hom_app_τ₃`, `HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso`, `Polynomial.Chebyshev.C_eval_neg_two`, `Polynomial.Chebyshev.T_eval_zero_of_even`, `CategoryTheory.CatCenter.app_neg_one_zpow`, `coe_negOnePow_natCast`, `CochainComplex.HomComplex.Cochain.δ_rightUnshift`, `negOnePow_zero`, `CochainComplex.HomComplex.Cochain.δ_rightShift`, `HomologicalComplex₂.ι_totalShift₂Iso_inv_f`, `CochainComplex.HomComplex.Cochain.leftShift_v`, `Matrix.submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det`, `ComplexShape.σ_def`, `CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₃`, `CochainComplex.HomComplex.Cochain.δ_leftUnshift`, `negOnePow_even`, `CochainComplex.shiftFunctor_obj_d'`, `HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom_assoc`, `CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso`, `CochainComplex.shiftShortComplexFunctor'_inv_app_τ₃`, `HomologicalComplex₂.ι_totalShift₂Iso_hom_f`, `CochainComplex.mappingCone.δ_descCochain`, `Polynomial.Chebyshev.one_lt_negOnePow_mul_eval_T_real`, `CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₂`, `Polynomial.Chebyshev.one_le_negOnePow_mul_eval_T_real`, `Polynomial.Chebyshev.T_eval_neg_one`, `ComplexShape.ε_up_ℤ`, `CochainComplex.shiftShortComplexFunctor'_inv_app_τ₁`, `CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃`, `HomologicalComplex₂.D₁_totalShift₂XIso_hom`, `HomologicalComplex₂.D₂_totalShift₂XIso_hom`, `Polynomial.Chebyshev.S_eval_neg_two`, `Function.Antiperiodic.int_mul_sub_eq`, `negOnePow_succ`, `CochainComplex.HomComplex.Cochain.δ_leftShift`, `CochainComplex.HomComplex.δ_zero_cochain_comp`, `negOnePow_eq_one_iff`, `CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁`, `cast_negOnePow_natCast`, `CochainComplex.shiftFunctor_obj_d`, `negOnePow_mul_self`, `Polynomial.Chebyshev.U_eval_zero_of_even`, `Polynomial.Chebyshev.eval_T_real_cos_int_mul_pi_div`, `Function.Antiperiodic.sub_zsmul_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_negOnePow` 📖	mathematical	—	`abs` `instLatticeInt` `instAddGroup` `Units.val` `instMonoid` `negOnePow`	—	`abs_eq_natAbs` `units_natAbs` `Nat.cast_one`
`cast_negOnePow_natCast` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `Units.val` `instMonoid` `negOnePow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`Nat.even_or_odd'` `Nat.instAtLeastTwoHAddOfNat` `Nat.cast_mul` `negOnePow_two_mul` `cast_one` `pow_mul` `pow_succ` `pow_zero` `mul_neg` `mul_one` `neg_neg` `one_pow` `Nat.cast_add` `Nat.cast_one` `negOnePow_two_mul_add_one` `cast_neg`
`coe_negOnePow_natCast` 📖	mathematical	—	`Units.val` `instMonoid` `negOnePow` `Monoid.toNatPow`	—	`cast_negOnePow_natCast`
`negOnePow_abs` 📖	mathematical	—	`negOnePow` `abs` `instLatticeInt` `instAddGroup`	—	`abs_choice` `negOnePow_neg`
`negOnePow_add` 📖	mathematical	—	`negOnePow` `Units` `instMonoid` `Units.instMul`	—	`zpow_add`
`negOnePow_def` 📖	mathematical	—	`negOnePow` `Units` `instMonoid` `instUnitsPow` `instCommSemiring` `AddCommGroup.toIntModule` `Additive` `Additive.addCommGroup` `Units.instCommGroupUnits` `instCommMonoid` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `Units.instOne`	—	—
`negOnePow_eq_iff` 📖	mathematical	—	`negOnePow` `Even`	—	`negOnePow_even` `even_sub` `negOnePow_eq_one_iff` `negOnePow_odd` `not_even_iff_odd` `negOnePow_eq_neg_one_iff` `not_odd_iff_even`
`negOnePow_eq_neg_one_iff` 📖	mathematical	—	`negOnePow` `Units` `instMonoid` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `Units.instOne` `Odd` `instSemiring`	—	`not_even_iff_odd` `negOnePow_even` `negOnePow_odd`
`negOnePow_eq_one_iff` 📖	mathematical	—	`negOnePow` `Units` `instMonoid` `Units.instOne` `Even`	—	`not_odd_iff_even` `negOnePow_odd` `negOnePow_even`
`negOnePow_even` 📖	mathematical	`Even`	`negOnePow` `Units` `instMonoid` `Units.instOne`	—	`negOnePow_add` `units_mul_self`
`negOnePow_mul_self` 📖	mathematical	—	`negOnePow`	—	`mul_sub` `mul_one` `even_mul_pred_self`
`negOnePow_neg` 📖	mathematical	—	`negOnePow`	—	`zpow_neg` `inv_neg` `inv_one`
`negOnePow_odd` 📖	mathematical	`Odd` `instSemiring`	`negOnePow` `Units` `instMonoid` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `Units.instOne`	—	`negOnePow_add` `negOnePow_two_mul` `mul_neg` `mul_one`
`negOnePow_one` 📖	mathematical	—	`negOnePow` `Units` `instMonoid` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `Units.instOne`	—	—
`negOnePow_sub` 📖	mathematical	—	`negOnePow` `Units` `instMonoid` `Units.instMul`	—	`sub_eq_add_neg` `negOnePow_add` `negOnePow_neg`
`negOnePow_succ` 📖	mathematical	—	`negOnePow` `Units` `instMonoid` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing`	—	`negOnePow_add` `negOnePow_one` `mul_neg` `mul_one`
`negOnePow_two_mul` 📖	mathematical	—	`negOnePow` `Units` `instMonoid` `Units.instOne`	—	`negOnePow_even` `two_mul`
`negOnePow_two_mul_add_one` 📖	mathematical	—	`negOnePow` `Units` `instMonoid` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `Units.instOne`	—	`negOnePow_odd`
`negOnePow_zero` 📖	mathematical	—	`negOnePow` `Units` `instMonoid` `Units.instOne`	—	—

---

← Back to Index