Theorems · Definition · group theory
intEquivOfZPowersEqTop
{G : Type u_2} → [Infinite G] → [inst : Group G] → (g : G) → Subgroup.zpowers g = ⊤ → Multiplicative ℤ ≃* GThe isomorphism between Multiplicative ℤ and the infinite cyclic group G sending
Multiplicative.ofAdd 1 to the generator g : G.
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Top.topstatement and proof · cited by 9,680
- Groupstatement and proof · cited by 6,238
- Subgroupstatement · cited by 3,593
- MulEquivstatement · cited by 1,142
- Multiplicativestatement · cited by 875
- Infinitestatement and proof · cited by 352
- Subgroup.zpowersstatement and proof · cited by 204
- zpowersHomproof · cited by 9
- MulEquiv.ofBijectiveproof · cited by 5
- zpowersHom_bijectiveproof · cited by 2
Cited by13
Results whose statement or proof uses this declaration.
- Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulIntproof · cited by 11
- Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_applystatement · cited by 3
- intEquivOfZPowersEqTop_applystatement and proof · cited by 2
- intEquivOfZPowersEqTop_symm_selfstatement and proof · cited by 1
- mulintEquivOfZPowersEqTop_strictMonostatement · cited by 1
- mulintEquivOfZPowersEqTop_symm_apply_zpowstatement and proof · cited by 1
- intEquivOfZPowersEqTop.congr_simpstatement and proof · cited by 1
- Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_symm_applystatement · cited by 0
- mulintEquivOfZPowersEqTop_strictAntistatement · cited by 0
- intCyclicMulEquivproof · cited by 0
- Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply_zeroproof · cited by 0