Theorems · Definition · commutative algebra
zpowersHom
(α : Type u_3) → [inst : Group α] → α ≃ (Multiplicative ℤ →* α)
Monoid homomorphisms from Multiplicative ℤ are defined by the image
of Multiplicative.ofAdd 1.
- Defined in
- Mathlib.Data.Int.Cast.Lemmas
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 43 from the axioms · uses propext, Quot.sound
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivstatement · cited by 8,337
- Groupstatement and proof · cited by 6,238
- MonoidHomstatement · cited by 3,629
- Multiplicativestatement · cited by 875
- Additiveproof · cited by 356
- Equiv.transproof · cited by 337
- Additive.ofMulproof · cited by 155
- zmultiplesHomproof · cited by 7
- AddMonoidHom.toMultiplicativeLeftproof · cited by 5
Cited by13
Results whose statement or proof uses this declaration.
- intEquivOfZPowersEqTopproof · cited by 11
- HNNExtension.liftproof · cited by 5
- zpowersHom_bijectivestatement and proof · cited by 2
- zpowersMulHomproof · cited by 2
- uliftZPowersHomproof · cited by 2
- zpowersHom_ker_eqstatement · cited by 1
- zpowersHom_symm_applystatement · cited by 1
- mulintEquivOfZPowersEqTop_strictMonoproof · cited by 1
- CircleDeg1Lift.units_semiconj_of_translationNumber_eqproof · cited by 1
- zpowersHom_applystatement · cited by 1
- Subgroup.range_zpowersHomstatement · cited by 0
- MonoidHom.apply_mintproof · cited by 0