Mathlib Map

Theorems · Theorem · group theory

Units.val_pow_eq_pow_val

∀ {α : Type u} [inst : Monoid α] (a : αˣ) (n : ℕ), ↑(a ^ n) = ↑a ^ n
Defined in
Mathlib.Algebra.Group.Units.Defs
Cited by
24 results in Mathlib
Foundations
Depth 18 from the axioms · uses propext
Assumes
Monoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsPrimitiveRoot.pow_of_coprime · cited by 8IsPrimitiveRoot.pow_of_co…FiniteField.pow_card_sub_one_eq_one · cited by 7FiniteField.pow_card_sub_…HasEnoughRootsOfUnity.natCard_rootsOfUnity · cited by 5HasEnoughRootsOfUnity.nat…Int.units_sq · cited by 5Int.units_sqrootsOfUnity.coe_pow · cited by 2rootsOfUnity.coe_powMulChar.pow_card_eq_one · cited by 2MulChar.pow_card_eq_oneMatrix.GeneralLinearGroup.IsParabolic.pow · cited by 2IsParabolic.powmodularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow · cited by 2modularCyclotomicCharacte…MulChar.apply_mem_algebraAdjoin_of_pow_eq_one · cited by 2MulChar.apply_mem_algebra…NNReal.exists_lt_of_strictMono · cited by 2NNReal.exists_lt_of_stric…WeierstrassCurve.coe_inv_variableChange_Δ' · cited by 1WeierstrassCurve.coe_inv_…DirichletCharacter.unit_norm_eq_one · cited by 1DirichletCharacter.unit_n…Complex.mem_rootsOfUnity · cited by 1Complex.mem_rootsOfUnityLaurentPolynomial.eval₂_T · cited by 1LaurentPolynomial.eval₂_Tmem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt · cited by 1mem_adjoin_of_smul_prime_…Monoid · cited by 3887MonoidUnits · cited by 2804UnitsUnits.val · cited by 1966Units.valUnits.val_pow_eq_pow_valCITED BYCITES

Cites3

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

  • Monoidstatement and proof · cited by 3,887
  • Unitsstatement and proof · cited by 2,804
  • Units.valstatement · cited by 1,966

Cited by24

Results whose statement or proof uses this declaration.