Mathlib Map

Theorems · Definition · number theory

Int.negOnePow

ℤ → ℤˣ

The map ℤ → ℤˣ which sends n to (-1 : ℤˣ) ^ n.

Defined in
Mathlib.Algebra.Ring.NegOnePow
Cited by
156 results in Mathlib
Foundations
Depth 40 from the axioms, rests on 595 definitions · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CochainComplex.HomComplex.δ · cited by 102HomComplex.δCochainComplex.shiftFunctor · cited by 50CochainComplex.shiftFunct…CategoryTheory.Pretriangulated.Triangle.shiftFunctor · cited by 31Triangle.shiftFunctorInt.negOnePow_add · cited by 25Int.negOnePow_addInt.coe_negOnePow · cited by 24Int.coe_negOnePowCochainComplex.HomComplex.Cochain.leftShift · cited by 23Cochain.leftShiftCochainComplex.HomComplex.Cochain.leftShift_v · cited by 19Cochain.leftShift_vInt.negOnePow_even · cited by 13Int.negOnePow_evenInt.negOnePow_neg · cited by 13Int.negOnePow_negCochainComplex.HomComplex.Cochain.leftUnshift · cited by 13Cochain.leftUnshiftCochainComplex.HomComplex.δ_v · cited by 13HomComplex.δ_vCochainComplex.mappingCocone.descCochain · cited by 12mappingCocone.descCochainCochainComplex.HomComplex.δ_shape · cited by 11HomComplex.δ_shapePowerSeries.pentagonalSeries · cited by 10PowerSeries.pentagonalSer…Int.cast_negOnePow · cited by 10Int.cast_negOnePowUnits · cited by 2804UnitsInt.negOnePowCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Unitsstatement · cited by 2,804

Cited by171

Results whose statement or proof uses this declaration.