Mathlib Map

Theorems · Theorem · number theory

Int.units_mul_self

∀ (u : ℤˣ), u * u = 1
Defined in
Mathlib.Data.Int.Order.Units
Cited by
27 results in Mathlib
Foundations
Depth 41 from the axioms · uses propext, Classical.choice
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Int.negOnePow_even · cited by 13Int.negOnePow_evenCategoryTheory.Functor.homologySequence_exact₂ · cited by 8Functor.homologySequence_…Matrix.det_succ_row · cited by 6Matrix.det_succ_rowInt.units_inv_eq_self · cited by 5Int.units_inv_eq_selfCochainComplex.mappingCocone.inl_v_descCochain_v · cited by 3mappingCocone.inl_v_descC…CochainComplex.mappingCocone.inr_v_descCochain_v · cited by 3mappingCocone.inr_v_descC…CochainComplex.HomComplex.Cochain.δ_leftShift · cited by 2Cochain.δ_leftShiftCochainComplex.HomComplex.Cochain.δ_rightShift · cited by 2Cochain.δ_rightShiftCochainComplex.HomComplex.Cochain.δ_rightUnshift · cited by 2Cochain.δ_rightUnshiftHomologicalComplex₂.D₂_totalShift₁XIso_hom · cited by 1HomologicalComplex₂.D₂_to…ComplexShape.ε₁_ε₂ · cited by 1ComplexShape.ε₁_ε₂CochainComplex.IsKInjective.eq_δ_of_cocycle · cited by 1IsKInjective.eq_δ_of_cocy…AlternatingMap.coe_alternatization · cited by 1AlternatingMap.coe_altern…CochainComplex.HomComplex.Cocycle.toSingleMk_mem_coboundaries_iff · cited by 1Cocycle.toSingleMk_mem_co…CochainComplex.HomComplex.Cocycle.toSingleMk_surjective · cited by 1Cocycle.toSingleMk_surjec…Units · cited by 2804Unitssq · cited by 280sqInt.units_sq · cited by 5Int.units_sqInt.units_mul_selfCITED BYCITES

Cites3

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

  • Unitsstatement and proof · cited by 2,804
  • sqproof · cited by 280
  • Int.units_sqproof · cited by 5

Cited by27

Results whose statement or proof uses this declaration.