Theorems · Theorem · group theory
Units.val_zpow_eq_zpow_val
∀ {α : Type u_1} [inst : DivisionMonoid α] (u : αˣ) (n : ℤ), ↑(u ^ n) = ↑u ^ n- Defined in
- Mathlib.Algebra.Group.Units.Hom
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 22 from the axioms · uses propext
- Assumes
- DivisionMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Unitsstatement · cited by 2,804
- Units.valstatement · cited by 1,966
- DivisionMonoidstatement and proof · cited by 201
- Units.coeHomproof · cited by 44
- MonoidHom.map_zpowproof · cited by 10
Cited by7
Results whose statement or proof uses this declaration.
- Valuation.exists_pow_Uniformizerproof · cited by 3
- Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_mem_rangeproof · cited by 2
- RatFunc.uniformizingPolynomial_isUniformizerproof · cited by 1
- autEquivZmod_symm_apply_intCastproof · cited by 1
- ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_of_nonzeroproof · cited by 1
- ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on_of_nonzeroproof · cited by 0