Loogle!

Result

Found 204 declarations mentioning Subgroup.zpowers. Of these, only the first 200 are shown.

Subgroup.zpowers 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] (g : G) : Subgroup G
Subgroup.mem_zpowers 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] (g : G) : g ∈ Subgroup.zpowers g
Subgroup.zpowers_eq_closure 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] (g : G) : Subgroup.zpowers g = Subgroup.closure {g}
Subgroup.decidableMemZPowers 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] {a : G} : DecidablePred fun x => x ∈ Subgroup.zpowers a
Subgroup.zpowers_inv 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] {g : G} : Subgroup.zpowers g⁻¹ = Subgroup.zpowers g
Subgroup.zpowers_one_eq_bot 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] : Subgroup.zpowers 1 = ⊥
Subgroup.zpowers_isMulCommutative 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] (g : G) : IsMulCommutative ↥(Subgroup.zpowers g)
Subgroup.zpowers_eq_bot 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] {g : G} : Subgroup.zpowers g = ⊥ ↔ g = 1
Subgroup.zpowers_ne_bot 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] {g : G} : Subgroup.zpowers g ≠ ⊥ ↔ g ≠ 1
Subgroup.zpow_mem_zpowers 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] (g : G) (k : ℤ) : g ^ k ∈ Subgroup.zpowers g
Subgroup.coe_zpowers 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] (g : G) : ↑(Subgroup.zpowers g) = Set.range fun x => g ^ x
Subgroup.npow_mem_zpowers 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] (g : G) (k : ℕ) : g ^ k ∈ Subgroup.zpowers g
Subgroup.zpowers_le_of_mem 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] {g : G} {H : Subgroup G} : g ∈ H → Subgroup.zpowers g ≤ H
Subgroup.zpowers_le 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] {g : G} {H : Subgroup G} : Subgroup.zpowers g ≤ H ↔ g ∈ H
Subgroup.forall_mem_zpowers 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] {x : G} {p : G → Prop} : (∀ g ∈ Subgroup.zpowers x, p g) ↔ ∀ (m : ℤ), p (x ^ m)
Subgroup.mem_zpowers_iff 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] {g h : G} : h ∈ Subgroup.zpowers g ↔ ∃ k, g ^ k = h
Subgroup.exists_mem_zpowers 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] {x : G} {p : G → Prop} : (∃ g ∈ Subgroup.zpowers x, p g) ↔ ∃ m, p (x ^ m)
Subgroup.zpowers_mul_le_sup 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] (g h : G) : Subgroup.zpowers (g * h) ≤ Subgroup.zpowers g ⊔ Subgroup.zpowers h
ofAdd_image_zmultiples_eq_zpowers_ofAdd 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{A : Type u_2} [AddGroup A] {x : A} : ⇑Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x) = ↑(Subgroup.zpowers (Multiplicative.ofAdd x))
ofMul_image_zpowers_eq_zmultiples_ofMul 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] {x : G} : ⇑Additive.ofMul '' ↑(Subgroup.zpowers x) = ↑(AddSubgroup.zmultiples (Additive.ofMul x))
MonoidHom.map_zpowers 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] {N : Type u_3} [Group N] (f : G →* N) (x : G) : Subgroup.map f (Subgroup.zpowers x) = Subgroup.zpowers (f x)
Subgroup.forall_zpowers 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] {x : G} {p : ↥(Subgroup.zpowers x) → Prop} : (∀ (g : ↥(Subgroup.zpowers x)), p g) ↔ ∀ (m : ℤ), p ⟨x ^ m, ⋯⟩
Subgroup.exists_zpowers 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
{G : Type u_1} [Group G] {x : G} {p : ↥(Subgroup.zpowers x) → Prop} : (∃ g, p g) ↔ ∃ m, p ⟨x ^ m, ⋯⟩
Submonoid.powers_le_zpowers 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
{G : Type u_2} [Group G] (g : G) : Submonoid.powers g ≤ (Subgroup.zpowers g).toSubmonoid
Subgroup.toSubmonoid_zpowers 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
{G : Type u_2} [Group G] (g : G) : (Subgroup.zpowers g).toSubmonoid = Submonoid.powers g ⊔ Submonoid.powers g⁻¹
IsOfFinOrder.of_mem_zpowers 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] {x y : G} (h : IsOfFinOrder x) (h' : y ∈ Subgroup.zpowers x) : IsOfFinOrder y
orderOf_dvd_of_mem_zpowers 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] {x y : G} (h : y ∈ Subgroup.zpowers x) : orderOf y ∣ orderOf x
finEquivZPowers 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] {x : G} (hx : IsOfFinOrder x) : Fin (orderOf x) ≃ ↥(Subgroup.zpowers x)
Subgroup.zpowers_eq_zpowers_iff 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] {x y : G} (hx : ¬IsOfFinOrder x) : Subgroup.zpowers x = Subgroup.zpowers y ↔ x = y ∨ x⁻¹ = y
powers_eq_zpowers 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] [Finite G] (x : G) : ↑(Submonoid.powers x) = ↑(Subgroup.zpowers x)
zpowers_mabs 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (g : G) : Subgroup.zpowers |g|ₘ = Subgroup.zpowers g
Fintype.card_zpowers 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] [Fintype G] {x : G} : Fintype.card ↥(Subgroup.zpowers x) = orderOf x
IsOfFinOrder.powers_eq_zpowers 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] {x : G} (hx : IsOfFinOrder x) : ↑(Submonoid.powers x) = ↑(Subgroup.zpowers x)
mem_zpowers_pow_iff 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] {g : G} {k : ℕ} : g ∈ Subgroup.zpowers (g ^ k) ↔ k.gcd (orderOf g) = 1
mem_zpowers_zpow_iff 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] {g : G} {k : ℤ} : g ∈ Subgroup.zpowers (g ^ k) ↔ k.gcd ↑(orderOf g) = 1
mem_powers_iff_mem_zpowers 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] {x y : G} [Finite G] : y ∈ Submonoid.powers x ↔ y ∈ Subgroup.zpowers x
zpowersEquivZPowers 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] {x y : G} [Finite G] (h : orderOf x = orderOf y) : ↥(Subgroup.zpowers x) ≃ ↥(Subgroup.zpowers y)
image_range_orderOf 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] [Fintype G] {x : G} [DecidableEq G] : Finset.image (fun i => x ^ i) (Finset.range (orderOf x)) = (↑(Subgroup.zpowers x)).toFinset
mem_zpowers_iff_mem_range_orderOf 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] {x y : G} [Finite G] [DecidableEq G] : y ∈ Subgroup.zpowers x ↔ y ∈ Finset.image (fun x_1 => x ^ x_1) (Finset.range (orderOf x))
IsOfFinOrder.mem_powers_iff_mem_zpowers 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] {x y : G} (hx : IsOfFinOrder x) : y ∈ Submonoid.powers x ↔ y ∈ Subgroup.zpowers x
IsOfFinOrder.mem_zpowers_iff_mem_range_orderOf 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] {x y : G} [DecidableEq G] (hx : IsOfFinOrder x) : y ∈ Subgroup.zpowers x ↔ y ∈ Finset.image (fun x_1 => x ^ x_1) (Finset.range (orderOf x))
card_zpowers_le 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] [Fintype G] (a : G) {k : ℕ} (k_pos : k ≠ 0) (ha : a ^ k = 1) : Fintype.card ↥(Subgroup.zpowers a) ≤ k
smul_eq_self_of_mem_zpowers 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] {x y : G} {α : Type u_6} [MulAction G α] (hx : x ∈ Subgroup.zpowers y) {a : α} (hs : y • a = a) : x • a = a
pow_finEquivZPowers_symm_apply 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] {x : G} (hx : IsOfFinOrder x) (a : ↥(Subgroup.zpowers x)) : x ^ ↑((finEquivZPowers hx).symm a) = ↑a
finEquivZPowers_apply 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] {x : G} (hx : IsOfFinOrder x) {n : Fin (orderOf x)} : (finEquivZPowers hx) n = ⟨x ^ ↑n, ⋯⟩
finEquivZPowers_symm_apply 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] {x : G} (hx : IsOfFinOrder x) (n : ℕ) : (finEquivZPowers hx).symm ⟨x ^ n, ⋯⟩ = ⟨n % orderOf x, ⋯⟩
zpowersEquivZPowers_apply 📋 Mathlib.GroupTheory.OrderOfElement
{G : Type u_1} [Group G] {x y : G} [Finite G] (h : orderOf x = orderOf y) (n : ℕ) : (zpowersEquivZPowers h) ⟨x ^ n, ⋯⟩ = ⟨y ^ n, ⋯⟩
Subgroup.instCountableSubtypeMemZpowers 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
{G : Type u_1} [Group G] (a : G) : Countable ↥(Subgroup.zpowers a)
Subgroup.finsetSup_zpowers 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
{G : Type u_1} [Group G] (s : Finset G) : s.sup Subgroup.zpowers = Subgroup.closure ↑s
Subgroup.range_zpowersHom 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
{G : Type u_1} [Group G] (g : G) : ((zpowersHom G) g).range = Subgroup.zpowers g
IsOfFinOrder.finite_zpowers 📋 Mathlib.Data.ZMod.QuotientGroup
{α : Type u_2} [Group α] {a : α} : IsOfFinOrder a → (↑(Subgroup.zpowers a)).Finite
finite_zpowers 📋 Mathlib.Data.ZMod.QuotientGroup
{α : Type u_2} [Group α] {a : α} : (↑(Subgroup.zpowers a)).Finite ↔ IsOfFinOrder a
infinite_zpowers 📋 Mathlib.Data.ZMod.QuotientGroup
{α : Type u_2} [Group α] {a : α} : (↑(Subgroup.zpowers a)).Infinite ↔ ¬IsOfFinOrder a
Nat.card_zpowers 📋 Mathlib.Data.ZMod.QuotientGroup
{α : Type u_2} [Group α] (a : α) : Nat.card ↥(Subgroup.zpowers a) = orderOf a
MulAction.orbitZPowersEquiv 📋 Mathlib.Data.ZMod.QuotientGroup
{α : Type u_2} {β : Type u_3} [Group α] (a : α) [MulAction α β] (b : β) : ↑(MulAction.orbit (↥(Subgroup.zpowers a)) b) ≃ ZMod (Function.minimalPeriod (fun x => a • x) b)
MulAction.minimalPeriod_pos 📋 Mathlib.Data.ZMod.QuotientGroup
{α : Type u_2} {β : Type u_3} [Group α] (a : α) [MulAction α β] (b : β) [Finite ↑(MulAction.orbit (↥(Subgroup.zpowers a)) b)] : NeZero (Function.minimalPeriod (fun x => a • x) b)
Subgroup.quotientEquivSigmaZMod 📋 Mathlib.Data.ZMod.QuotientGroup
{G : Type u_2} [Group G] (H : Subgroup G) (g : G) : G ⧸ H ≃ (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)) × ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q))
MulAction.minimalPeriod_eq_card 📋 Mathlib.Data.ZMod.QuotientGroup
{α : Type u_2} {β : Type u_3} [Group α] (a : α) [MulAction α β] (b : β) [Fintype ↑(MulAction.orbit (↥(Subgroup.zpowers a)) b)] : Function.minimalPeriod (fun x => a • x) b = Fintype.card ↑(MulAction.orbit (↥(Subgroup.zpowers a)) b)
Subgroup.index_eq_sum_minimalPeriod 📋 Mathlib.Data.ZMod.QuotientGroup
{G : Type u_2} [Group G] (H : Subgroup G) (g : G) [Finite (G ⧸ H)] [Fintype (Quotient (MulAction.orbitRel (↥(Subgroup.zpowers g)) (G ⧸ H)))] : H.index = ∑ q, Function.minimalPeriod (fun x => g • x) q.out
MulAction.zpowersQuotientStabilizerEquiv 📋 Mathlib.Data.ZMod.QuotientGroup
{α : Type u_2} {β : Type u_3} [Group α] (a : α) [MulAction α β] (b : β) : ↥(Subgroup.zpowers a) ⧸ MulAction.stabilizer (↥(Subgroup.zpowers a)) b ≃* Multiplicative (ZMod (Function.minimalPeriod (fun x => a • x) b))
MulAction.orbitZPowersEquiv_symm_apply 📋 Mathlib.Data.ZMod.QuotientGroup
{α : Type u_2} {β : Type u_3} [Group α] (a : α) [MulAction α β] (b : β) (k : ZMod (Function.minimalPeriod (fun x => a • x) b)) : (MulAction.orbitZPowersEquiv a b).symm k = ⟨a, ⋯⟩ ^ k.cast • ⟨b, ⋯⟩
MulAction.orbitZPowersEquiv_symm_apply' 📋 Mathlib.Data.ZMod.QuotientGroup
{α : Type u_2} {β : Type u_3} [Group α] (a : α) [MulAction α β] (b : β) (k : ℤ) : (MulAction.orbitZPowersEquiv a b).symm ↑k = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩
Subgroup.quotientEquivSigmaZMod_symm_apply 📋 Mathlib.Data.ZMod.QuotientGroup
{G : Type u_2} [Group G] (H : Subgroup G) (g : G) (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)) (k : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q))) : (H.quotientEquivSigmaZMod g).symm ⟨q, k⟩ = g ^ k.cast • Quotient.out q
Subgroup.quotientEquivSigmaZMod_apply 📋 Mathlib.Data.ZMod.QuotientGroup
{G : Type u_2} [Group G] (H : Subgroup G) (g : G) (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)) (k : ℤ) : (H.quotientEquivSigmaZMod g) (g ^ k • Quotient.out q) = ⟨q, ↑k⟩
MulAction.zpowersQuotientStabilizerEquiv_symm_apply 📋 Mathlib.Data.ZMod.QuotientGroup
{α : Type u_2} {β : Type u_3} [Group α] (a : α) [MulAction α β] (b : β) (n : ZMod (Function.minimalPeriod (fun x => a • x) b)) : (MulAction.zpowersQuotientStabilizerEquiv a b).symm n = ↑⟨a, ⋯⟩ ^ n.cast
isCyclic_iff_exists_zpowers_eq_top 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
{α : Type u_1} [Group α] : IsCyclic α ↔ ∃ g, Subgroup.zpowers g = ⊤
orderOf_eq_card_of_zpowers_eq_top 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
{G : Type u_2} [Group G] {g : G} (h : Subgroup.zpowers g = ⊤) : orderOf g = Nat.card G
Subgroup.isCyclic_zpowers 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
{G : Type u_2} [Group G] (g : G) : IsCyclic ↥(Subgroup.zpowers g)
IsCyclic.exists_generator 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
{α : Type u_1} [Group α] [IsCyclic α] : ∃ g, ∀ (x : α), x ∈ Subgroup.zpowers g
orderOf_eq_card_of_forall_mem_zpowers 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
{α : Type u_1} [Group α] {g : α} (hx : ∀ (x : α), x ∈ Subgroup.zpowers g) : orderOf g = Nat.card α
Infinite.orderOf_eq_zero_of_forall_mem_zpowers 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
{α : Type u_1} [Group α] [Infinite α] {g : α} (h : ∀ (x : α), x ∈ Subgroup.zpowers g) : orderOf g = 0
Subgroup.isCyclic_iff_exists_zpowers_eq_top 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
{α : Type u_1} [Group α] (H : Subgroup α) : IsCyclic ↥H ↔ ∃ g, Subgroup.zpowers g = H
zpowers_eq_top_of_prime_card 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
{G : Type u_2} [Group G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g : G} (hg : g ≠ 1) : Subgroup.zpowers g = ⊤
mem_zpowers_of_prime_card 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
{G : Type u_2} [Group G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g g' : G} (hg : g ≠ 1) : g' ∈ Subgroup.zpowers g
Subgroup.le_zpowers_iff 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
{G : Type u_2} [Group G] (g : G) (H : Subgroup G) : H ≤ Subgroup.zpowers g ↔ ∃ n, H = Subgroup.zpowers (g ^ n)
IsCyclic.image_range_card 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
{α : Type u_1} {a : α} [Group α] [Fintype α] [DecidableEq α] (ha : ∀ (x : α), x ∈ Subgroup.zpowers a) : Finset.image (fun i => a ^ i) (Finset.range (Nat.card α)) = Finset.univ
IsCyclic.unique_zpow_zmod 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
{α : Type u_1} {a : α} [Group α] [Fintype α] (ha : ∀ (x : α), x ∈ Subgroup.zpowers a) (x : α) : ∃! n, x = a ^ n.val
IsCyclic.image_range_orderOf 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
{α : Type u_1} {a : α} [Group α] [Fintype α] [DecidableEq α] (ha : ∀ (x : α), x ∈ Subgroup.zpowers a) : Finset.image (fun i => a ^ i) (Finset.range (orderOf a)) = Finset.univ
Equiv.Perm.IsCycle.zpowersEquivSupport 📋 Mathlib.GroupTheory.Perm.Cycle.Basic
{α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} (hσ : σ.IsCycle) : ↥(Subgroup.zpowers σ) ≃ ↥σ.support
Equiv.Perm.IsCycle.commute_iff' 📋 Mathlib.GroupTheory.Perm.Cycle.Basic
{α : Type u_2} [Fintype α] [DecidableEq α] {g c : Equiv.Perm α} (hc : c.IsCycle) : Commute g c ↔ ∃ (hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support), g.subtypePerm hc' ∈ Subgroup.zpowers c.subtypePermOfSupport
Equiv.Perm.IsCycle.commute_iff 📋 Mathlib.GroupTheory.Perm.Cycle.Basic
{α : Type u_2} [Fintype α] [DecidableEq α] {g c : Equiv.Perm α} (hc : c.IsCycle) : Commute g c ↔ ∃ (hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support), Equiv.Perm.ofSubtype (g.subtypePerm hc') ∈ Subgroup.zpowers c
Equiv.Perm.IsCycle.zpowersEquivSupport_apply 📋 Mathlib.GroupTheory.Perm.Cycle.Basic
{α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} (hσ : σ.IsCycle) {n : ℕ} : hσ.zpowersEquivSupport ⟨σ ^ n, ⋯⟩ = ⟨(σ ^ n) (Classical.choose hσ), ⋯⟩
Equiv.Perm.IsCycle.zpowersEquivSupport_symm_apply 📋 Mathlib.GroupTheory.Perm.Cycle.Basic
{α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} (hσ : σ.IsCycle) (n : ℕ) : hσ.zpowersEquivSupport.symm ⟨(σ ^ n) (Classical.choose hσ), ⋯⟩ = ⟨σ ^ n, ⋯⟩
Equiv.Perm.support_zpowers_of_mem_cycleFactorsFinset_le 📋 Mathlib.GroupTheory.Perm.Cycle.Factors
{α : Type u_1} [DecidableEq α] [Fintype α] {g : Equiv.Perm α} {c : ↥g.cycleFactorsFinset} (v : ↥(Subgroup.zpowers ↑c)) : (↑v).support ⊆ g.support
Equiv.Perm.pairwise_disjoint_of_mem_zpowers 📋 Mathlib.GroupTheory.Perm.Cycle.Factors
{α : Type u_1} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) : Pairwise fun i j => ∀ (x y : Equiv.Perm α), x ∈ Subgroup.zpowers ↑i → y ∈ Subgroup.zpowers ↑j → x.Disjoint y
Equiv.Perm.pairwise_commute_of_mem_zpowers 📋 Mathlib.GroupTheory.Perm.Cycle.Factors
{α : Type u_1} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) : Pairwise fun i j => ∀ (x y : Equiv.Perm α), x ∈ Subgroup.zpowers ↑i → y ∈ Subgroup.zpowers ↑j → Commute x y
Equiv.Perm.commute_iff_of_mem_cycleFactorsFinset 📋 Mathlib.GroupTheory.Perm.Cycle.Factors
{α : Type u_1} [DecidableEq α] [Fintype α] {g k c : Equiv.Perm α} (hc : c ∈ g.cycleFactorsFinset) : Commute k c ↔ ∃ (hc' : ∀ (x : α), k x ∈ c.support ↔ x ∈ c.support), k.subtypePerm hc' ∈ Subgroup.zpowers (g.subtypePerm ⋯)
Equiv.Perm.IsCycle.forall_commute_iff 📋 Mathlib.GroupTheory.Perm.Cycle.Factors
{α : Type u_1} [DecidableEq α] [Fintype α] (g z : Equiv.Perm α) : (∀ c ∈ g.cycleFactorsFinset, Commute z c) ↔ ∀ c ∈ g.cycleFactorsFinset, ∃ (hc : ∀ (x : α), z x ∈ c.support ↔ x ∈ c.support), Equiv.Perm.ofSubtype (z.subtypePerm hc) ∈ Subgroup.zpowers c
Equiv.Perm.disjoint_ofSubtype_noncommPiCoprod 📋 Mathlib.GroupTheory.Perm.Cycle.Factors
{α : Type u_1} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (u : Equiv.Perm ↑(Function.fixedPoints ⇑f)) (v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)) : (Equiv.Perm.ofSubtype u).Disjoint ((Subgroup.noncommPiCoprod ⋯) v)
Equiv.Perm.commute_ofSubtype_noncommPiCoprod 📋 Mathlib.GroupTheory.Perm.Cycle.Factors
{α : Type u_1} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (u : Equiv.Perm ↑(Function.fixedPoints ⇑f)) (v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)) : Commute (Equiv.Perm.ofSubtype u) ((Subgroup.noncommPiCoprod ⋯) v)
intEquivOfZPowersEqTop 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Infinite G] [Group G] (g : G) (hg : Subgroup.zpowers g = ⊤) : Multiplicative ℤ ≃* G
Subgroup.relIndex_zpowers_zpow 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Group G] (g : G) (i : ℤ) : (Subgroup.zpowers (g ^ i)).relIndex (Subgroup.zpowers g) = i.gcd ↑(orderOf g)
Subgroup.index_zpowers_zpow 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Group G] {g : G} (hg : Subgroup.zpowers g = ⊤) (i : ℤ) : (Subgroup.zpowers (g ^ i)).index = i.gcd ↑(orderOf g)
zmodMulEquivOfGenerator 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Group G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n) : Multiplicative (ZMod n) ≃* G
Subgroup.zpowers_le_zpowers_of_dvd 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Group G] (g : G) {m n : ℤ} (h : n ∣ m) : Subgroup.zpowers (g ^ m) ≤ Subgroup.zpowers (g ^ n)
monoidHomOfForallMemZpowers 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {g' : G'} (hg' : orderOf g' ∣ orderOf g) : G →* G'
Subgroup.zpowers_eq_zpowers_iff' 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Group G] (g : G) (i j : ℤ) : Subgroup.zpowers (g ^ i) = Subgroup.zpowers (g ^ j) ↔ i.gcd ↑(orderOf g) = j.gcd ↑(orderOf g)
Subgroup.relIndex_zpowers_zpow_zpow 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Group G] (g : G) (i j : ℤ) : (Subgroup.zpowers (g ^ i)).relIndex (Subgroup.zpowers (g ^ j)) * (i.gcd j).gcd (orderOf g) = i.gcd ↑(orderOf g)
mulEquivOfOrderOfEq 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {g' : G'} (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') (h : orderOf g = orderOf g') : G ≃* G'
Subgroup.zpowers_le_zpowers_iff 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Group G] (g : G) (i j : ℤ) : Subgroup.zpowers (g ^ i) ≤ Subgroup.zpowers (g ^ j) ↔ j.gcd ↑(orderOf g) ∣ i.gcd ↑(orderOf g)
Subgroup.zpowers_zpow_sup 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Group G] (g : G) (i j : ℤ) : Subgroup.zpowers (g ^ i) ⊔ Subgroup.zpowers (g ^ j) = Subgroup.zpowers (g ^ ↑(i.gcd j))
monoidHomOfForallMemZpowers_apply_gen 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {g' : G'} (hg' : orderOf g' ∣ orderOf g) : (monoidHomOfForallMemZpowers hg hg') g = g'
intEquivOfZPowersEqTop_apply 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Infinite G] [Group G] (g : G) (hg : Subgroup.zpowers g = ⊤) (a : Multiplicative ℤ) : (intEquivOfZPowersEqTop g hg) a = g ^ Multiplicative.toAdd a
intEquivOfZPowersEqTop_symm_self 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Infinite G] [Group G] {g : G} (hg : Subgroup.zpowers g = ⊤) : (intEquivOfZPowersEqTop g hg).symm g = Multiplicative.ofAdd 1
mulintEquivOfZPowersEqTop_strictAnti 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Infinite G] [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] {g : G} (hg : Subgroup.zpowers g = ⊤) (hg1 : g < 1) : StrictAnti ⇑(intEquivOfZPowersEqTop g hg)
mulintEquivOfZPowersEqTop_strictMono 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Infinite G] [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] {g : G} (hg : Subgroup.zpowers g = ⊤) (hg1 : 1 < g) : StrictMono ⇑(intEquivOfZPowersEqTop g hg)
mulintEquivOfZPowersEqTop_symm_apply_zpow 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Infinite G] [Group G] {g : G} (hg : Subgroup.zpowers g = ⊤) (k : ℤ) : (intEquivOfZPowersEqTop g hg).symm (g ^ k) = Multiplicative.ofAdd k
mulEquivOfOrderOfEq_symm 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {g' : G'} (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') (h : orderOf g = orderOf g') : (mulEquivOfOrderOfEq hg hg' h).symm = mulEquivOfOrderOfEq hg' hg ⋯
mulEquivOfOrderOfEq_apply_gen 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {g' : G'} (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') (h : orderOf g = orderOf g') : (mulEquivOfOrderOfEq hg hg' h) g = g'
mulEquivOfOrderOfEq_symm_apply_gen 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {g' : G'} (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') (h : orderOf g = orderOf g') : (mulEquivOfOrderOfEq hg hg' h).symm g' = g
zpowersHom_ker_eq 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Group G] (g : G) : ((zpowersHom G) g).ker = Subgroup.zpowers (Multiplicative.ofAdd ↑(orderOf g))
MonoidHom.eq_iff_eq_on_generator 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (f₁ f₂ : G →* G') : f₁ = f₂ ↔ f₁ g = f₂ g
zpowersHom_bijective 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Infinite G] [Group G] {g : G} (hg : Subgroup.zpowers g = ⊤) : Function.Bijective ⇑((zpowersHom G) g)
zmodMulEquivOfGenerator_apply_ofAdd_one 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Group G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n) : (zmodMulEquivOfGenerator hg hn) (Multiplicative.ofAdd 1) = g
zmodMulEquivOfGenerator_apply_ofAdd_intCast 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Group G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n) (i : ℤ) : (zmodMulEquivOfGenerator hg hn) (Multiplicative.ofAdd ↑i) = g ^ i
zmodMulEquivOfGenerator_symm_apply_generator 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Group G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n) : (zmodMulEquivOfGenerator hg hn).symm g = Multiplicative.ofAdd 1
zmodMulEquivOfGenerator_symm_apply_zpow 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} [Group G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n) (i : ℤ) : (zmodMulEquivOfGenerator hg hn).symm (g ^ i) = Multiplicative.ofAdd ↑i
MulEquiv.eq_iff_eq_on_generator 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
{G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (f₁ f₂ : G ≃* G') : f₁ = f₂ ↔ f₁ g = f₂ g
IsCyclic.monoidHomMulEquivRootsOfUnityOfGenerator 📋 Mathlib.RingTheory.RootsOfUnity.Basic
{G : Type u_7} [CommGroup G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (G' : Type u_8) [CommGroup G'] : (G →* G') ≃* ↥(rootsOfUnity (Nat.card G) G')
Representation.apply_eq_of_leftRegular_eq_of_generator 📋 Mathlib.RepresentationTheory.Basic
{k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (x : MonoidAlgebra k G) (hx : ((Representation.leftRegular k G) g) x = x) (γ : G) : x.coeff γ = x.coeff g
Representation.coeff_of_leftRegular_of_generator 📋 Mathlib.RepresentationTheory.Basic
{k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (x : MonoidAlgebra k G) (hx : ((Representation.leftRegular k G) g) x = x) (γ : G) : x.coeff γ = x.coeff g
Subgroup.dense_iff_ne_zpowers 📋 Mathlib.Topology.Algebra.Order.Archimedean
{G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] [Nontrivial G] [DenselyOrdered G] {s : Subgroup G} : Dense ↑s ↔ ∀ (a : G), s ≠ Subgroup.zpowers a
Subgroup.dense_xor'_cyclic 📋 Mathlib.Topology.Algebra.Order.Archimedean
{G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] [Nontrivial G] [DenselyOrdered G] (s : Subgroup G) : Xor (Dense ↑s) (∃ a, s = Subgroup.zpowers a)
Subgroup.dense_xor_cyclic 📋 Mathlib.Topology.Algebra.Order.Archimedean
{G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] [Nontrivial G] [DenselyOrdered G] (s : Subgroup G) : Xor (Dense ↑s) (∃ a, s = Subgroup.zpowers a)
LinearOrderedCommGroup.genLTOne_unique 📋 Mathlib.Algebra.Order.Group.Cyclic
(G : Type u_1) [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [Nontrivial G] [IsCyclic G] {g : G} (hg : g < 1) (htop : Subgroup.zpowers g = ⊤) : g = LinearOrderedCommGroup.genLTOne G
LinearOrderedCommGroup.Subgroup.genLTOne_zpowers_eq_top 📋 Mathlib.Algebra.Order.Group.Cyclic
{G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (H : Subgroup G) [Nontrivial ↥H] [hH : IsCyclic ↥H] : Subgroup.zpowers (LinearOrderedCommGroup.Subgroup.genLTOne H) = H
LinearOrderedCommGroup.Subgroup.genLTOne_unique_of_zpowers_eq 📋 Mathlib.Algebra.Order.Group.Cyclic
{G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {g1 g2 : G} (hg1 : g1 < 1) (hg2 : g2 < 1) (h : Subgroup.zpowers g1 = Subgroup.zpowers g2) : g1 = g2
LinearOrderedCommGroup.Subgroup.exists_generator_lt_one 📋 Mathlib.Algebra.Order.Group.Cyclic
{G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (H : Subgroup G) [Nontrivial ↥H] [hH : IsCyclic ↥H] : ∃ a < 1, Subgroup.zpowers a = H
LinearOrderedCommGroup.Subgroup.genLTOne_unique 📋 Mathlib.Algebra.Order.Group.Cyclic
{G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (H : Subgroup G) [Nontrivial ↥H] [hH : IsCyclic ↥H] {g : G} (hg : g < 1) : Subgroup.zpowers g = H → g = LinearOrderedCommGroup.Subgroup.genLTOne H
Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup 📋 Mathlib.RingTheory.Valuation.Discrete.Basic
{Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] (v : Valuation A Γ) [v.IsRankOneDiscrete] : Subgroup.zpowers (Valuation.IsRankOneDiscrete.generator v) = (MonoidWithZeroHom.ofClass v).valueGroup
Valuation.IsUniformizer.zpowers_eq_valueGroup 📋 Mathlib.RingTheory.Valuation.Discrete.Basic
{Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] {v : Valuation A Γ} [hv : v.IsRankOneDiscrete] {π : A} (hπ : v.IsUniformizer π) : (MonoidWithZeroHom.ofClass v).valueGroup = Subgroup.zpowers (Units.mk0 (v π) ⋯)
Valuation.IsRankOneDiscrete.generator_zpowers_eq_range 📋 Mathlib.RingTheory.Valuation.Discrete.Basic
{Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] (K : Type u_3) [Field K] (w : Valuation K Γ) [w.IsRankOneDiscrete] : Units.val '' ↑(Subgroup.zpowers (Valuation.IsRankOneDiscrete.generator w)) = Set.range ⇑w \ {0}
Valuation.IsRankOneDiscrete.exists_generator_lt_one 📋 Mathlib.RingTheory.Valuation.Discrete.Basic
{Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] (v : Valuation A Γ) [v.IsRankOneDiscrete] : ∃ γ, Subgroup.zpowers γ = (MonoidWithZeroHom.ofClass v).valueGroup ∧ γ < 1
Valuation.IsRankOneDiscrete.exists_generator_lt_one' 📋 Mathlib.RingTheory.Valuation.Discrete.Basic
{Γ : Type u_1} {inst✝ : LinearOrderedCommGroupWithZero Γ} {A : Type u_2} {inst✝¹ : Ring A} {v : Valuation A Γ} [self : v.IsRankOneDiscrete] : ∃ γ, Subgroup.zpowers γ = (MonoidWithZeroHom.ofClass v).valueGroup ∧ γ < 1
Valuation.IsRankOneDiscrete.mk 📋 Mathlib.RingTheory.Valuation.Discrete.Basic
{Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] {v : Valuation A Γ} (exists_generator_lt_one' : ∃ γ, Subgroup.zpowers γ = (MonoidWithZeroHom.ofClass v).valueGroup ∧ γ < 1) : v.IsRankOneDiscrete
Valuation.IsRankOneDiscrete.generator'_zpowers_eq_top 📋 Mathlib.RingTheory.Valuation.Discrete.Basic
{Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] (v : Valuation A Γ) [v.IsRankOneDiscrete] : Subgroup.zpowers (Valuation.IsRankOneDiscrete.generator' v) = ⊤
IsPrimitiveRoot.zpowers_eq 📋 Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
{R : Type u_4} [CommRing R] [IsDomain R] {k : ℕ} [NeZero k] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) : Subgroup.zpowers ζ = rootsOfUnity k R
IsPrimitiveRoot.zmodEquivZPowers 📋 Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
{R : Type u_4} {k : ℕ} [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) : ZMod k ≃+ Additive ↥(Subgroup.zpowers ζ)
IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow' 📋 Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
{R : Type u_4} {k : ℕ} [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℤ) : h.zmodEquivZPowers.symm ⟨ζ ^ i, ⋯⟩ = ↑i
IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow' 📋 Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
{R : Type u_4} {k : ℕ} [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℕ) : h.zmodEquivZPowers.symm ⟨ζ ^ i, ⋯⟩ = ↑i
IsPrimitiveRoot.zmodEquivZPowers_apply_coe_int 📋 Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
{R : Type u_4} {k : ℕ} [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℤ) : h.zmodEquivZPowers ↑i = Additive.ofMul ⟨ζ ^ i, ⋯⟩
IsPrimitiveRoot.zmodEquivZPowers_apply_coe_nat 📋 Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
{R : Type u_4} {k : ℕ} [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℕ) : h.zmodEquivZPowers ↑i = Additive.ofMul ⟨ζ ^ i, ⋯⟩
IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow 📋 Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
{R : Type u_4} {k : ℕ} [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℤ) : h.zmodEquivZPowers.symm (Additive.ofMul ⟨ζ ^ i, ⋯⟩) = ↑i
IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow 📋 Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
{R : Type u_4} {k : ℕ} [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℕ) : h.zmodEquivZPowers.symm (Additive.ofMul ⟨ζ ^ i, ⋯⟩) = ↑i
MulChar.eq_iff 📋 Mathlib.NumberTheory.MulChar.Lemmas
{R : Type u_1} [CommMonoid R] {R' : Type u_3} [CommMonoidWithZero R'] {g : Rˣ} (hg : ∀ (x : Rˣ), x ∈ Subgroup.zpowers g) (χ₁ χ₂ : MulChar R R') : χ₁ = χ₂ ↔ χ₁ ↑g = χ₂ ↑g
MulChar.ofRootOfUnity 📋 Mathlib.NumberTheory.MulChar.Lemmas
{M : Type u_1} [CommMonoid M] [Fintype M] [DecidableEq M] {R : Type u_2} [CommMonoidWithZero R] {ζ : Rˣ} (hζ : ζ ∈ rootsOfUnity (Fintype.card Mˣ) R) {g : Mˣ} (hg : ∀ (x : Mˣ), x ∈ Subgroup.zpowers g) : MulChar M R
MulChar.ofRootOfUnity_spec 📋 Mathlib.NumberTheory.MulChar.Lemmas
{M : Type u_1} [CommMonoid M] [Fintype M] [DecidableEq M] {R : Type u_2} [CommMonoidWithZero R] {ζ : Rˣ} (hζ : ζ ∈ rootsOfUnity (Fintype.card Mˣ) R) {g : Mˣ} (hg : ∀ (x : Mˣ), x ∈ Subgroup.zpowers g) : (MulChar.ofRootOfUnity hζ hg) ↑g = ↑ζ
MeasureTheory.smul_ae_eq_self_of_mem_zpowers 📋 Mathlib.MeasureTheory.Group.AEStabilizer
{G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] {x y : G} {s : Set α} (hs : x • s =ᵐ[μ] s) (hy : y ∈ Subgroup.zpowers x) : y • s =ᵐ[μ] s
DihedralGroup.center_eq_closure_of_even_ne_two 📋 Mathlib.GroupTheory.SpecificGroups.Dihedral
{n : ℕ} (heven : Even n) (hn2 : n ≠ 2) : Subgroup.center (DihedralGroup n) = Subgroup.zpowers (DihedralGroup.r ↑(n / 2))
MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot 📋 Mathlib.GroupTheory.Transfer
{G : Type u_1} [Group G] {H : Subgroup G} {A : Type u_2} [CommGroup A] (ϕ : ↥H →* A) [H.FiniteIndex] (g : G) [Fintype (Quotient (MulAction.orbitRel (↥(Subgroup.zpowers g)) (G ⧸ H)))] : ϕ.transfer g = ∏ q, ϕ ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) q.out * Quotient.out q.out, ⋯⟩
Subgroup.transferTransversal_apply' 📋 Mathlib.GroupTheory.Transfer
{G : Type u_1} [Group G] {H : Subgroup G} (g : G) (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)) (k : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q))) : ↑(⋯.leftQuotientEquiv (g ^ k.cast • Quotient.out q)) = g ^ k.cast * Quotient.out (Quotient.out q)
Subgroup.transferTransversal_apply'' 📋 Mathlib.GroupTheory.Transfer
{G : Type u_1} [Group G] {H : Subgroup G} (g : G) (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)) (k : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q))) : ↑(⋯.leftQuotientEquiv (g ^ k.cast • Quotient.out q)) = if k = 0 then g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out q) * Quotient.out (Quotient.out q) else g ^ k.cast * Quotient.out (Quotient.out q)
Subgroup.transferFunction_apply 📋 Mathlib.GroupTheory.Transfer
{G : Type u_1} [Group G] {H : Subgroup G} (g : G) (q : G ⧸ H) : H.transferFunction g q = g ^ ((H.quotientEquivSigmaZMod g) q).snd.cast * Quotient.out (Quotient.out ((H.quotientEquivSigmaZMod g) q).fst)
Equiv.Perm.OnCycleFactors.kerParam_range_le_centralizer 📋 Mathlib.GroupTheory.Perm.Centralizer
{α : Type u_1} [DecidableEq α] [Fintype α] {g : Equiv.Perm α} : (Equiv.Perm.OnCycleFactors.kerParam g).range ≤ Subgroup.centralizer {g}
Equiv.Perm.OnCycleFactors.kerParam 📋 Mathlib.GroupTheory.Perm.Centralizer
{α : Type u_1} [DecidableEq α] [Fintype α] (g : Equiv.Perm α) : Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)) →* Equiv.Perm α
Equiv.Perm.OnCycleFactors.kerParam_range_eq 📋 Mathlib.GroupTheory.Perm.Centralizer
{α : Type u_1} [DecidableEq α] [Fintype α] {g : Equiv.Perm α} : (Equiv.Perm.OnCycleFactors.kerParam g).range = Subgroup.map (Subgroup.centralizer {g}).subtype (Equiv.Perm.OnCycleFactors.toPermHom g).ker
Equiv.Perm.OnCycleFactors.kerParam_range_card 📋 Mathlib.GroupTheory.Perm.Centralizer
{α : Type u_1} [DecidableEq α] [Fintype α] (g : Equiv.Perm α) : Fintype.card ↥(Equiv.Perm.OnCycleFactors.kerParam g).range = (Fintype.card α - g.cycleType.sum).factorial * g.cycleType.prod
Equiv.Perm.OnCycleFactors.kerParam_injective 📋 Mathlib.GroupTheory.Perm.Centralizer
{α : Type u_1} [DecidableEq α] [Fintype α] (g : Equiv.Perm α) : Function.Injective ⇑(Equiv.Perm.OnCycleFactors.kerParam g)
Equiv.Perm.OnCycleFactors.cycleType_kerParam_apply_apply 📋 Mathlib.GroupTheory.Perm.Centralizer
{α : Type u_1} [DecidableEq α] [Fintype α] (g : Equiv.Perm α) (k : Equiv.Perm ↑(Function.fixedPoints ⇑g)) (v : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)) : ((Equiv.Perm.OnCycleFactors.kerParam g) (k, v)).cycleType = k.cycleType + ∑ c, (↑(v c)).cycleType
Equiv.Perm.OnCycleFactors.sign_kerParam_apply_apply 📋 Mathlib.GroupTheory.Perm.Centralizer
{α : Type u_1} [DecidableEq α] [Fintype α] (g : Equiv.Perm α) (k : Equiv.Perm ↑(Function.fixedPoints ⇑g)) (v : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)) : Equiv.Perm.sign ((Equiv.Perm.OnCycleFactors.kerParam g) (k, v)) = Equiv.Perm.sign k * ∏ c, Equiv.Perm.sign ↑(v c)
Equiv.Perm.OnCycleFactors.kerParam_apply 📋 Mathlib.GroupTheory.Perm.Centralizer
{α : Type u_1} [DecidableEq α] [Fintype α] {g : Equiv.Perm α} {u : Equiv.Perm ↑(Function.fixedPoints ⇑g)} {v : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)} {x : α} : ((Equiv.Perm.OnCycleFactors.kerParam g) (u, v)) x = if hx : g.cycleOf x ∈ g.cycleFactorsFinset then ↑(v ⟨g.cycleOf x, hx⟩) x else (Equiv.Perm.ofSubtype u) x
Equiv.Perm.OnCycleFactors.kerParam_range_eq_centralizer_of_count_le_one 📋 Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
{α : Type u_1} [Fintype α] [DecidableEq α] {g : Equiv.Perm α} (h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1) : (Equiv.Perm.OnCycleFactors.kerParam g).range = Subgroup.centralizer {g}
Subgroup.instDiscreteTopologyZMultiples 📋 Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
{G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] (g : G) : DiscreteTopology ↥(Subgroup.zpowers g)
NumberField.IsCMField.zpowers_complexConj_eq_top 📋 Mathlib.NumberTheory.NumberField.CMField
(K : Type u_1) [Field K] [CharZero K] [NumberField.IsCMField K] [Algebra.IsIntegral ℚ K] : Subgroup.zpowers (NumberField.IsCMField.complexConj K) = ⊤
NumberField.IsCMField.indexRealUnits_eq_two_iff 📋 Mathlib.NumberTheory.NumberField.CMField
(K : Type u_1) [Field K] [CharZero K] [NumberField.IsCMField K] [NumberField K] : NumberField.IsCMField.indexRealUnits K = 2 ↔ ∃ u, Subgroup.zpowers ((NumberField.IsCMField.unitsMulComplexConjInv K) u) = ⊤
IsCyclotomicExtension.Rat.galEquivZMod_stabilizer 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
(n : ℕ) [NeZero n] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] (p : ℕ) [hp : Fact (Nat.Prime p)] (P : Ideal (NumberField.RingOfIntegers K)) [P.IsMaximal] [P.LiesOver (Ideal.span {↑p})] (hn : p.Coprime n) : (IsCyclotomicExtension.Rat.galEquivZMod n K).mapSubgroup (MulAction.stabilizer Gal(K/ℚ) P) = Subgroup.zpowers (ZMod.unitOfCoprime p hn)
IsCyclotomicExtension.Rat.mem_zpowers_galEquivZMod_of_mem_stabilizer 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
(n : ℕ) [NeZero n] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] (p : ℕ) [hp : Fact (Nat.Prime p)] (P : Ideal (NumberField.RingOfIntegers K)) [P.IsMaximal] [P.LiesOver (Ideal.span {↑p})] (hn : p.Coprime n) {σ : Gal(K/ℚ)} (hσ : σ ∈ MulAction.stabilizer Gal(K/ℚ) P) : (IsCyclotomicExtension.Rat.galEquivZMod n K) σ ∈ Subgroup.zpowers (ZMod.unitOfCoprime p hn)
Representation.mem_invariants_iff_of_forall_mem_zpowers 📋 Mathlib.RepresentationTheory.Invariants
{k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (x : V) : x ∈ ρ.invariants ↔ (ρ g) x = x
Rep.FiniteCyclicGroup.resolution 📋 Mathlib.RepresentationTheory.Homological.FiniteCyclic
(k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : CategoryTheory.ProjectiveResolution (Rep.trivial k G k)
Rep.FiniteCyclicGroup.resolution_complex 📋 Mathlib.RepresentationTheory.Homological.FiniteCyclic
(k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : (Rep.FiniteCyclicGroup.resolution k g hg).complex = (Rep.FiniteCyclicGroup.chainComplexFunctor k g).obj (Rep.leftRegular k G)
Representation.FiniteCyclicGroup.coinvariantsKer_eq_range 📋 Mathlib.RepresentationTheory.Homological.FiniteCyclic
{k : Type u_1} {G : Type u_2} [CommRing k] [Group G] {V : Type u_4} [AddCommGroup V] [Module k V] (ρ : Representation k G V) (g : G) [Finite G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : Representation.Coinvariants.ker ρ = (ρ g - LinearMap.id).range
Rep.FiniteCyclicGroup.resolution_π 📋 Mathlib.RepresentationTheory.Homological.FiniteCyclic
(k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : (Rep.FiniteCyclicGroup.resolution k g hg).π = Rep.FiniteCyclicGroup.resolution.π k g
Rep.FiniteCyclicGroup.resolution_quasiIso 📋 Mathlib.RepresentationTheory.Homological.FiniteCyclic
(k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : QuasiIso (Rep.FiniteCyclicGroup.resolution.π k g)
Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination 📋 Mathlib.RepresentationTheory.Homological.FiniteCyclic
(k : Type u) {G : Type u} [CommRing k] [CommGroup G] (g : G) [Finite G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : (Rep.Hom.hom ((Rep.leftRegular k G).applyAsHom g - CategoryTheory.CategoryStruct.id (Rep.leftRegular k G))).range = ((Finsupp.linearCombination k fun x => 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker
Representation.FiniteCyclicGroup.coinvariantsEquiv 📋 Mathlib.RepresentationTheory.Homological.FiniteCyclic
{k : Type u_1} {G : Type u_2} [CommRing k] [Group G] {V : Type u_4} [AddCommGroup V] [Module k V] (ρ : Representation k G V) (g : G) [Fintype G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : ρ.Coinvariants ≃ₗ[k] V ⧸ (ρ g - LinearMap.id).range
Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm 📋 Mathlib.RepresentationTheory.Homological.FiniteCyclic
(k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : (Rep.Hom.hom ((Rep.leftRegular k G).applyAsHom g - CategoryTheory.CategoryStruct.id (Rep.leftRegular k G))).range = (Rep.Hom.hom (Rep.leftRegular k G).norm).ker
Rep.FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub 📋 Mathlib.RepresentationTheory.Homological.FiniteCyclic
(k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : (Rep.Hom.hom (Rep.leftRegular k G).norm).range = (Rep.Hom.hom ((Rep.leftRegular k G).applyAsHom g - CategoryTheory.CategoryStruct.id (Rep.leftRegular k G))).ker
Rep.FiniteCyclicGroup.groupCohomologyIsoOdd 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) : groupCohomology A i ≅ (Rep.FiniteCyclicGroup.subCompNormHom A g).homology
Rep.FiniteCyclicGroup.groupCohomologyIsoEven 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [h₀ : NeZero i] (hi : Even i) : groupCohomology A i ≅ (Rep.FiniteCyclicGroup.normHomCompSub A g).homology
Rep.FiniteCyclicGroup.homResolutionIso 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : (Rep.FiniteCyclicGroup.resolution k g hg).complex.linearYonedaObj k A ≅ Rep.FiniteCyclicGroup.moduleCatCochainComplex A g
Rep.FiniteCyclicGroup.groupCohomologyπOdd 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) : ModuleCat.of k ↥(Rep.Hom.hom A.norm).ker ⟶ groupCohomology A i
Rep.FiniteCyclicGroup.groupCohomologyIso₀ 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : groupCohomology A 0 ≅ ModuleCat.of k ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker
Rep.FiniteCyclicGroup.groupCohomologyπEven 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [NeZero i] (hi : Even i) : ModuleCat.of k ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker ⟶ groupCohomology A i
Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (x : Rep.leftRegular k G ⟶ A) : (ModuleCat.Hom.hom ((Rep.FiniteCyclicGroup.homResolutionIso A g hg).hom.f i)) x = (Rep.homEquiv x) (MonoidAlgebra.single 1 1)
Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (a : ↑A) (x : MonoidAlgebra k G) : (Rep.Hom.hom ((ModuleCat.Hom.hom ((Rep.FiniteCyclicGroup.homResolutionIso A g hg).inv.f i)) a)) x = x.coeff.sum fun x r => r • (A.ρ x) a
Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) (x : ↥(Rep.Hom.hom A.norm).ker) : (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπOdd A g hg i hi)) x = 0 ↔ ↑x ∈ (Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).range
Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [NeZero i] (hi : Even i) (x : ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker) : (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπEven A g hg i hi)) x = 0 ↔ ↑x ∈ (Rep.Hom.hom A.norm).range
Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_iff 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) (x y : ↥(Rep.Hom.hom A.norm).ker) : (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπOdd A g hg i hi)) x = (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπOdd A g hg i hi)) y ↔ ↑x - ↑y ∈ (Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).range
Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_iff 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [NeZero i] (hi : Even i) (x y : ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker) : (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπEven A g hg i hi)) x = (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπEven A g hg i hi)) y ↔ ↑x - ↑y ∈ (Rep.Hom.hom A.norm).range
groupCohomology.exists_div_of_norm_eq_one 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
{K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [IsCyclic Gal(L/K)] {g : Gal(L/K)} (hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g) {x : L} (hx : (Algebra.norm K) x = 1) : ∃ y, ↑y / g ↑y = x
groupCohomology.exists_mul_galRestrict_of_norm_eq_one 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
{K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [IsCyclic Gal(L/K)] {g : Gal(L/K)} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [Algebra A L] [Algebra A K] [Algebra B L] [IsScalarTower A B L] [IsScalarTower A K L] [IsFractionRing A K] [IsDomain A] [IsIntegralClosure B A L] (hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g) {η : B} (hη : (Algebra.norm K) ((algebraMap B L) η) = 1) : ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) g) ε = ε
Rep.FiniteCyclicGroup.groupHomologyIsoOdd 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) [DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) : groupHomology A i ≅ (Rep.FiniteCyclicGroup.normHomCompSub A g).homology
Rep.FiniteCyclicGroup.groupHomologyIsoEven 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) [DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [h₀ : NeZero i] (hi : Even i) : groupHomology A i ≅ (Rep.FiniteCyclicGroup.subCompNormHom A g).homology
Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : HomologicalComplex.coinvariantsTensorObj A (Rep.FiniteCyclicGroup.resolution k g⁻¹ ⋯).complex ≅ Rep.FiniteCyclicGroup.moduleCatChainComplex A g
Rep.FiniteCyclicGroup.groupHomologyπEven 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) [DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [NeZero i] (hi : Even i) : ModuleCat.of k ↥(LinearMap.ker A.ρ.norm) ⟶ groupHomology A i
Rep.FiniteCyclicGroup.groupHomologyIso₀ 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : groupHomology A 0 ≅ ModuleCat.of k (↑A ⧸ (Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).range)
Rep.FiniteCyclicGroup.groupHomologyπOdd 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) [DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) : ModuleCat.of k ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker ⟶ groupHomology A i
Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) [DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [NeZero i] (hi : Even i) (x : ↥(LinearMap.ker A.ρ.norm)) : (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupHomologyπEven A g hg i hi)) x = 0 ↔ ↑x ∈ (Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).range
Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) [DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) (x : ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker) : (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupHomologyπOdd A g hg i hi)) x = 0 ↔ ↑x ∈ LinearMap.range A.ρ.norm
Rep.FiniteCyclicGroup.groupHomologyπEven_eq_iff 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) [DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [NeZero i] (hi : Even i) (x y : ↥(LinearMap.ker A.ρ.norm)) : (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupHomologyπEven A g hg i hi)) x = (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupHomologyπEven A g hg i hi)) y ↔ ↑x - ↑y ∈ (Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).range

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c