ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Monoid M<VAR>MulAction M α<GOAL>Antitone fun P => MulAction.fixedPoints (↥P) α
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Monoid M<VAR>MulAction M α<VAR>s t : Set α<GOAL>fixingSubmonoid M (s ∪ t) = fixingSubmonoid M s ⊓ fixingSubmonoid M t
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Monoid M<VAR>MulAction M α<VAR>ι : Sort u_3<VAR>s : ι → Set α<GOAL>fixingSubmonoid M (⋃ i, s i) = ⨅ i, fixingSubmonoid M (s i)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Monoid M<VAR>MulAction M α<VAR>P Q : Submonoid M<GOAL>MulAction.fixedPoints (↥(P ⊔ Q)) α = MulAction.fixedPoints (↥P) α ∩ MulAction.fixedPoints (↥Q) α
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Monoid M<VAR>MulAction M α<VAR>ι : Sort u_3<VAR>P : ι → Submonoid M<GOAL>MulAction.fixedPoints (↥(iSup P)) α = ⋂ i, MulAction.fixedPoints (↥(P i)) α
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Group M<VAR>MulAction M α<VAR>s : Set α<VAR>m : M<GOAL>m ∈ fixingSubgroup M s ↔ ∀ y ∈ s, m • y = y
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Group M<VAR>MulAction M α<VAR>s : Set α<VAR>m : M<GOAL>m ∈ fixingSubgroup M s ↔ s ⊆ MulAction.fixedBy α m
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Group M<VAR>MulAction M α<VAR>s : Set α<VAR>m : M<GOAL>m ∈ fixingSubgroup M sᶜ ↔ (MulAction.fixedBy α m)ᶜ ⊆ s
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Group M<VAR>MulAction M α<GOAL>GaloisConnection (⇑OrderDual.toDual ∘ fixingSubgroup M) ((fun P => MulAction.fixedPoints (↥P) α) ∘ ⇑OrderDual.ofDual)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Group M<VAR>MulAction M α<GOAL>Antitone (fixingSubgroup M)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Group M<VAR>MulAction M α<GOAL>Antitone fun P => MulAction.fixedPoints (↥P) α
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Group M<VAR>MulAction M α<VAR>s t : Set α<GOAL>fixingSubgroup M (s ∪ t) = fixingSubgroup M s ⊓ fixingSubgroup M t
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Group M<VAR>MulAction M α<VAR>ι : Sort u_3<VAR>s : ι → Set α<GOAL>fixingSubgroup M (⋃ i, s i) = ⨅ i, fixingSubgroup M (s i)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Group M<VAR>MulAction M α<VAR>P Q : Subgroup M<GOAL>MulAction.fixedPoints (↥(P ⊔ Q)) α = MulAction.fixedPoints (↥P) α ∩ MulAction.fixedPoints (↥Q) α
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Group M<VAR>MulAction M α<VAR>ι : Sort u_3<VAR>P : ι → Subgroup M<GOAL>MulAction.fixedPoints (↥(iSup P)) α = ⋂ i, MulAction.fixedPoints (↥(P i)) α
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Group M<VAR>MulAction M α<VAR>s : Set α<VAR>a : α<VAR>a_in_s : a ∈ s<GOAL>MulAction.orbit (↥(fixingSubgroup M sᶜ)) a ⊆ s
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>m : M<VAR>a : α<VAR>n : ℕ<VAR>period_pos : 0 < MulAction.period m a<VAR>moved : ∀ (k : ℕ), 0 < k → k < n → m ^ k • a ≠ a<GOAL>n ≤ MulAction.period m a
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>m : M<VAR>a : α<VAR>n : ℕ<VAR>period_pos : 0 < AddAction.period m a<VAR>moved : ∀ (k : ℕ), 0 < k → k < n → k • m +ᵥ a ≠ a<GOAL>n ≤ AddAction.period m a
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>m : M<VAR>a : α<VAR>n : ℕ<VAR>n_pos : 0 < n<VAR>fixed : n • m +ᵥ a = a<GOAL>AddAction.period m a ≤ n
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>m : M<VAR>a : α<VAR>n : ℕ<VAR>n_pos : 0 < n<VAR>fixed : m ^ n • a = a<GOAL>MulAction.period m a ≤ n
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>m : M<VAR>a : α<VAR>n : ℕ<VAR>n_pos : 0 < n<VAR>fixed : m ^ n • a = a<GOAL>0 < MulAction.period m a
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>m : M<VAR>a : α<VAR>n : ℕ<VAR>n_pos : 0 < n<VAR>fixed : n • m +ᵥ a = a<GOAL>0 < AddAction.period m a
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>m : M<VAR>a : α<GOAL>MulAction.period m a = 1 ↔ m • a = a
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>m : M<VAR>a : α<GOAL>AddAction.period m a = 1 ↔ m +ᵥ a = a
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>m : M<VAR>a : α<VAR>n : ℕ<VAR>n_pos : 0 < n<VAR>n_lt_period : n < MulAction.period m a<GOAL>m ^ n • a ≠ a
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>m : M<VAR>a : α<VAR>n : ℕ<VAR>n_pos : 0 < n<VAR>n_lt_period : n < AddAction.period m a<GOAL>n • m +ᵥ a ≠ a
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>a : α<GOAL>MulAction.period 1 a = 1
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>a : α<GOAL>AddAction.period 0 a = 1
<VAR>α : Type v<VAR>G : Type u<VAR>Group G<VAR>MulAction G α<VAR>g : G<VAR>a : α<GOAL>MulAction.period g⁻¹ a = MulAction.period g a
<VAR>α : Type v<VAR>G : Type u<VAR>AddGroup G<VAR>AddAction G α<VAR>g : G<VAR>a : α<GOAL>AddAction.period (-g) a = AddAction.period g a
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>m : M<VAR>a : α<GOAL>AddAction.period m a ∣ addOrderOf m
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>m : M<VAR>a : α<GOAL>MulAction.period m a ∣ orderOf m
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>m : M<VAR>order_pos : 0 < addOrderOf m<VAR>a : α<GOAL>0 < AddAction.period m a
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>m : M<VAR>order_pos : 0 < orderOf m<VAR>a : α<GOAL>0 < MulAction.period m a
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>m : M<VAR>order_pos : 0 < orderOf m<VAR>a : α<GOAL>MulAction.period m a ≤ orderOf m
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>m : M<VAR>order_pos : 0 < addOrderOf m<VAR>a : α<GOAL>AddAction.period m a ≤ addOrderOf m
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>m : M<VAR>a : α<GOAL>MulAction.period m a ∣ Monoid.exponent M
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>m : M<VAR>a : α<GOAL>AddAction.period m a ∣ AddMonoid.exponent M
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>exp_pos : 0 < AddMonoid.exponent M<VAR>m : M<VAR>a : α<GOAL>0 < AddAction.period m a
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>exp_pos : 0 < Monoid.exponent M<VAR>m : M<VAR>a : α<GOAL>0 < MulAction.period m a
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>exp_pos : 0 < AddMonoid.exponent M<VAR>m : M<VAR>a : α<GOAL>AddAction.period m a ≤ AddMonoid.exponent M
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>exp_pos : 0 < Monoid.exponent M<VAR>m : M<VAR>a : α<GOAL>MulAction.period m a ≤ Monoid.exponent M
<VAR>α : Type v<VAR>M : Type u<VAR>Monoid M<VAR>MulAction M α<VAR>exp_pos : 0 < Monoid.exponent M<VAR>m : M<GOAL>BddAbove (Set.range fun a => MulAction.period m a)
<VAR>α : Type v<VAR>M : Type u<VAR>AddMonoid M<VAR>AddAction M α<VAR>exp_pos : 0 < AddMonoid.exponent M<VAR>m : M<GOAL>BddAbove (Set.range fun a => AddAction.period m a)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Monoid R<VAR>MulAction R M<VAR>One M<GOAL>↑1 = Set.range fun r => r • 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Monoid R<VAR>MulAction R M<VAR>One M<VAR>x : M<GOAL>x ∈ 1 ↔ ∃ r, r • 1 = x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Monoid R<VAR>MulAction R M<VAR>One M<GOAL>1 ⊆ ↑1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Monoid R<VAR>MulAction R M<VAR>Mul M<VAR>IsScalarTower R M M<VAR>p q : SubMulAction R M<GOAL>↑(p * q) = ↑p * ↑q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Monoid R<VAR>MulAction R M<VAR>Mul M<VAR>IsScalarTower R M M<VAR>p q : SubMulAction R M<VAR>x : M<GOAL>x ∈ p * q ↔ ∃ y ∈ p, ∃ z ∈ q, y * z = x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Monoid R<VAR>MulAction R M<VAR>Monoid M<VAR>IsScalarTower R M M<VAR>SMulCommClass R M M<VAR>p : SubMulAction R M<VAR>n : ℕ<GOAL>n ≠ 0 → ↑(p ^ n) = ↑p ^ n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Monoid R<VAR>MulAction R M<VAR>Monoid M<VAR>IsScalarTower R M M<VAR>SMulCommClass R M M<VAR>p : SubMulAction R M<VAR>n : ℕ<GOAL>↑p ^ n ⊆ ↑(p ^ n)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>g : G<GOAL>MulAction.fixedBy α g⁻¹ = MulAction.fixedBy α g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>g : G<GOAL>AddAction.fixedBy α (-g) = AddAction.fixedBy α g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>a : α<VAR>g : G<GOAL>g • a ∈ MulAction.fixedBy α g ↔ a ∈ MulAction.fixedBy α g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>a : α<VAR>g : G<GOAL>g +ᵥ a ∈ AddAction.fixedBy α g ↔ a ∈ AddAction.fixedBy α g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>a : α<VAR>g : G<GOAL>-g +ᵥ a ∈ AddAction.fixedBy α g ↔ a ∈ AddAction.fixedBy α g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>a : α<VAR>g : G<GOAL>g⁻¹ • a ∈ MulAction.fixedBy α g ↔ a ∈ MulAction.fixedBy α g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>a : α<VAR>g : G<GOAL>Function.minimalPeriod (fun x => g • x) a = 1 ↔ a ∈ MulAction.fixedBy α g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>a : α<VAR>g : G<GOAL>Function.minimalPeriod (fun x => g +ᵥ x) a = 1 ↔ a ∈ AddAction.fixedBy α g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>g : G<VAR>j : ℤ<GOAL>AddAction.fixedBy α g ⊆ AddAction.fixedBy α (j • g)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>g : G<VAR>j : ℤ<GOAL>MulAction.fixedBy α g ⊆ MulAction.fixedBy α (g ^ j)
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>AddMonoid M<VAR>AddAction M α<GOAL>AddAction.fixedBy α 0 = Set.univ
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>MulAction M α<GOAL>MulAction.fixedBy α 1 = Set.univ
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>MulAction M α<VAR>m₁ m₂ : M<GOAL>MulAction.fixedBy α m₁ ∩ MulAction.fixedBy α m₂ ⊆ MulAction.fixedBy α (m₁ * m₂)
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>AddMonoid M<VAR>AddAction M α<VAR>m₁ m₂ : M<GOAL>AddAction.fixedBy α m₁ ∩ AddAction.fixedBy α m₂ ⊆ AddAction.fixedBy α (m₁ + m₂)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>g h : G<GOAL>h +ᵥ AddAction.fixedBy α g = AddAction.fixedBy α (h + g + -h)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>g h : G<GOAL>h • MulAction.fixedBy α g = MulAction.fixedBy α (h * g * h⁻¹)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>s : Set α<VAR>g : G<GOAL>s ∈ AddAction.fixedBy (Set α) g ↔ ∀ (x : α), g +ᵥ x ∈ s ↔ x ∈ s
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>s : Set α<VAR>g : G<GOAL>s ∈ MulAction.fixedBy (Set α) g ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>s : Set α<VAR>g : G<VAR>s_in_fixedBy : s ∈ MulAction.fixedBy (Set α) g<VAR>x : α<GOAL>g • x ∈ s ↔ x ∈ s
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>s : Set α<VAR>g : G<VAR>s_ss_fixedBy : s ⊆ MulAction.fixedBy α g<GOAL>s ∈ MulAction.fixedBy (Set α) g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>s : Set α<VAR>g : G<VAR>s_ss_fixedBy : s ⊆ AddAction.fixedBy α g<GOAL>s ∈ AddAction.fixedBy (Set α) g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>s t : Set α<VAR>g : G<VAR>t_ss_s : t ⊆ s<VAR>s_in_fixedBy : s ∈ MulAction.fixedBy (Set α) g<GOAL>g • t ⊆ s
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>s : Set α<VAR>g : G<VAR>s_subset : (MulAction.fixedBy α g)ᶜ ⊆ s<GOAL>s ∈ MulAction.fixedBy (Set α) g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>s : Set α<VAR>g : G<VAR>s_subset : (AddAction.fixedBy α g)ᶜ ⊆ s<GOAL>s ∈ AddAction.fixedBy (Set α) g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>g h : G<VAR>comm : AddCommute g h<GOAL>AddAction.fixedBy α g ∈ AddAction.fixedBy (Set α) h
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>g h : G<VAR>comm : Commute g h<GOAL>MulAction.fixedBy α g ∈ MulAction.fixedBy (Set α) h
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>g h : G<VAR>comm : AddCommute g h<VAR>j : ℤ<GOAL>j • h +ᵥ AddAction.fixedBy α g = AddAction.fixedBy α g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>g h : G<VAR>comm : Commute g h<VAR>j : ℤ<GOAL>h ^ j • MulAction.fixedBy α g = MulAction.fixedBy α g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>g h : G<VAR>comm : AddCommute g h<GOAL>(AddAction.fixedBy α g)ᶜ ∈ AddAction.fixedBy (Set α) h
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>g h : G<VAR>comm : Commute g h<GOAL>(MulAction.fixedBy α g)ᶜ ∈ MulAction.fixedBy (Set α) h
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>g h : G<VAR>comm : Commute g h<VAR>j : ℤ<GOAL>h ^ j • (MulAction.fixedBy α g)ᶜ = (MulAction.fixedBy α g)ᶜ
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>g h : G<VAR>comm : AddCommute g h<VAR>j : ℤ<GOAL>j • h +ᵥ (AddAction.fixedBy α g)ᶜ = (AddAction.fixedBy α g)ᶜ
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>AddMonoid M<VAR>AddAction M α<VAR>FaithfulVAdd M α<VAR>m : M<GOAL>AddAction.fixedBy α m = Set.univ ↔ m = 0
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>MulAction M α<VAR>FaithfulSMul M α<VAR>m : M<GOAL>MulAction.fixedBy α m = Set.univ ↔ m = 1
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>FaithfulSMul G α<VAR>g h : G<VAR>ne_one : g ≠ 1<VAR>disjoint : Disjoint (MulAction.fixedBy α g)ᶜ (h • (MulAction.fixedBy α g)ᶜ)<GOAL>¬Commute g h
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>FaithfulVAdd G α<VAR>g h : G<VAR>ne_one : g ≠ 0<VAR>disjoint : Disjoint (AddAction.fixedBy α g)ᶜ (h +ᵥ (AddAction.fixedBy α g)ᶜ)<GOAL>¬AddCommute g h
<VAR>G : Type u_1<VAR>CommGroup G<VAR>Group.FG G<GOAL>Nat.card G ∣ Monoid.exponent G ^ Group.rank G
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>AddGroup.FG G<GOAL>Nat.card G ∣ AddMonoid.exponent G ^ AddGroup.rank G
<VAR>G : Type u_1<VAR>CommGroup G<VAR>Group.FG G<VAR>n : ℕ<VAR>hG : ∀ (g : G), g ^ n = 1<GOAL>Nat.card G ∣ n ^ Group.rank G
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>AddGroup.FG G<VAR>n : ℕ<VAR>hG : ∀ (g : G), n • g = 0<GOAL>Nat.card G ∣ n ^ AddGroup.rank G
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>hR : R ∈ Subgroup.rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : Subgroup.closure S = ⊤<GOAL>↑(Subgroup.closure ((fun g => g * (↑(Subgroup.MemRightTransversals.toFun hR g))⁻¹) '' (R * S))) * R = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>hR : R ∈ Subgroup.rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : Subgroup.closure S = ⊤<GOAL>Subgroup.closure ((fun g => g * (↑(Subgroup.MemRightTransversals.toFun hR g))⁻¹) '' (R * S)) = H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>hR : R ∈ Subgroup.rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : Subgroup.closure S = ⊤<GOAL>Subgroup.closure ((fun g => ⟨g * (↑(Subgroup.MemRightTransversals.toFun hR g))⁻¹, ⋯⟩) '' (R * S)) = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>DecidableEq G<VAR>R S : Finset G<VAR>hR : ↑R ∈ Subgroup.rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : Subgroup.closure ↑S = ⊤<GOAL>Subgroup.closure ↑(Finset.image (fun g => ⟨g * (↑(Subgroup.MemRightTransversals.toFun hR g))⁻¹, ⋯⟩) (R * S)) = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>H.FiniteIndex<VAR>S : Finset G<VAR>hS : Subgroup.closure ↑S = ⊤<GOAL>∃ T, T.card ≤ H.index * S.card ∧ Subgroup.closure ↑T = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>hG : Group.FG G<VAR>H.FiniteIndex<GOAL>Group.rank ↥H ≤ H.index * Group.rank G
<VAR>G : Type u_1<VAR>Group G<VAR>Finite ↑(commutatorSet G)<GOAL>Nat.card ↥(commutator G) ∣ (Subgroup.center G).index ^ ((Subgroup.center G).index * Nat.card ↑(commutatorSet G) + 1)
<VAR>G : Type u_1<VAR>Group G<VAR>Finite ↑(commutatorSet G)<GOAL>Nat.card ↥(commutator G) ≤ Subgroup.cardCommutatorBound (Nat.card ↑(commutatorSet G))
<VAR>M : Type u_1<VAR>Monoid M<VAR>α : Type u_2<VAR>MulAction M α<VAR>m : M<VAR>hm : IsUnit m<GOAL>Function.Bijective fun a => m • a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_6<VAR>Monoid R<VAR>Monoid S<VAR>σ : R → S<VAR>MulAction R M<VAR>MulAction S N<VAR>F : Type u_7<VAR>h : F<VAR>FunLike F M N<VAR>MulActionSemiHomClass F σ M N<VAR>c : R<VAR>s : Set M<GOAL>⇑h '' (c • s) = σ c • ⇑h '' s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_6<VAR>Monoid R<VAR>Monoid S<VAR>σ : R → S<VAR>MulAction R M<VAR>MulAction S N<VAR>F : Type u_7<VAR>h : F<VAR>FunLike F M N<VAR>MulActionSemiHomClass F σ M N<VAR>c : R<VAR>t : Set N<GOAL>c • ⇑h ⁻¹' t ⊆ ⇑h ⁻¹' (σ c • t)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_6<VAR>Monoid R<VAR>Monoid S<VAR>σ : R → S<VAR>MulAction R M<VAR>MulAction S N<VAR>F : Type u_7<VAR>h : F<VAR>FunLike F M N<VAR>MulActionSemiHomClass F σ M N<VAR>c : R<VAR>t : Set N<VAR>hc : Function.Surjective fun m => c • m<VAR>hc' : Function.Injective fun n => σ c • n<GOAL>⇑h ⁻¹' (σ c • t) = c • ⇑h ⁻¹' t
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_6<VAR>Monoid R<VAR>Monoid S<VAR>σ : R → S<VAR>MulAction R M<VAR>MulAction S N<VAR>F : Type u_7<VAR>h : F<VAR>FunLike F M N<VAR>MulActionSemiHomClass F σ M N<VAR>c : R<VAR>t : Set N<VAR>hc : IsUnit c<VAR>hc' : IsUnit (σ c)<GOAL>⇑h ⁻¹' (σ c • t) = c • ⇑h ⁻¹' t
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_6<VAR>Monoid R<VAR>Monoid S<VAR>MulAction R M<VAR>MulAction S N<VAR>σ : R →* S<VAR>F : Type u_8<VAR>FunLike F M N<VAR>MulActionSemiHomClass F (⇑σ) M N<VAR>h : F<VAR>c : R<VAR>hc : IsUnit c<VAR>t : Set N<GOAL>⇑h ⁻¹' (σ c • t) = c • ⇑h ⁻¹' t
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_6<VAR>Monoid R<VAR>Monoid S<VAR>MulAction R M<VAR>MulAction S N<VAR>G : Type u_8<VAR>FunLike G R S<VAR>MonoidHomClass G R S<VAR>σ : G<VAR>F : Type u_9<VAR>FunLike F M N<VAR>MulActionSemiHomClass F (⇑σ) M N<VAR>h : F<VAR>c : R<VAR>hc : IsUnit c<VAR>t : Set N<GOAL>⇑h ⁻¹' (σ c • t) = c • ⇑h ⁻¹' t
<VAR>M : Type u_3<VAR>N : Type u_6<VAR>R : Type u_8<VAR>S : Type u_9<VAR>Group R<VAR>Group S<VAR>σ : R → S<VAR>MulAction R M<VAR>MulAction S N<VAR>F : Type u_10<VAR>FunLike F M N<VAR>MulActionSemiHomClass F σ M N<VAR>h : F<VAR>c : R<VAR>t : Set N<GOAL>⇑h ⁻¹' (σ c • t) = c • ⇑h ⁻¹' t
<VAR>R : Type u_1<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>Monoid R<VAR>MulAction R M₁<VAR>MulAction R M₂<VAR>F : Type u_7<VAR>h : F<VAR>FunLike F M₁ M₂<VAR>MulActionHomClass F R M₁ M₂<VAR>c : R<VAR>s : Set M₁<GOAL>⇑h '' (c • s) = c • ⇑h '' s
<VAR>R : Type u_1<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>Monoid R<VAR>MulAction R M₁<VAR>MulAction R M₂<VAR>F : Type u_7<VAR>h : F<VAR>FunLike F M₁ M₂<VAR>MulActionHomClass F R M₁ M₂<VAR>c : R<VAR>t : Set M₂<GOAL>c • ⇑h ⁻¹' t ⊆ ⇑h ⁻¹' (c • t)
<VAR>R : Type u_1<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>Monoid R<VAR>MulAction R M₁<VAR>MulAction R M₂<VAR>F : Type u_7<VAR>h : F<VAR>FunLike F M₁ M₂<VAR>MulActionHomClass F R M₁ M₂<VAR>c : R<VAR>t : Set M₂<VAR>hc : IsUnit c<GOAL>⇑h ⁻¹' (c • t) = c • ⇑h ⁻¹' t
<VAR>R : Type u_8<VAR>Group R<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>MulAction R M₁<VAR>MulAction R M₂<VAR>F : Type u_11<VAR>FunLike F M₁ M₂<VAR>MulActionHomClass F R M₁ M₂<VAR>h : F<VAR>c : R<VAR>t : Set M₂<GOAL>⇑h ⁻¹' (c • t) = c • ⇑h ⁻¹' t
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>Commensurable H H
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<GOAL>Commensurable H K ↔ Commensurable K H
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<GOAL>Commensurable H K → Commensurable K H
<VAR>G : Type u_1<VAR>Group G<VAR>H K L : Subgroup G<VAR>hhk : Commensurable H K<VAR>hkl : Commensurable K L<GOAL>Commensurable H L
<VAR>G : Type u_1<VAR>Group G<GOAL>Equivalence Commensurable
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>g : ConjAct G<GOAL>Commensurable H K ↔ Commensurable (g • H) (g • K)
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>g : ConjAct G<GOAL>Commensurable (g • H) H ↔ Commensurable H (g⁻¹ • H)
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>g : ConjAct G<GOAL>g ∈ Commensurable.commensurator' H ↔ Commensurable (g • H) H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>g : G<GOAL>g ∈ Commensurable.commensurator H ↔ Commensurable (ConjAct.toConjAct g • H) H
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>hk : Commensurable H K<GOAL>Commensurable.commensurator H = Commensurable.commensurator K
<VAR>G : Type u_3<VAR>Fintype G<GOAL>Fintype.card (ConjAct G) = Fintype.card G
<VAR>G : Type u_3<VAR>DivInvMonoid G<VAR>p : ConjAct G → Prop<GOAL>(∀ (x : ConjAct G), p x) ↔ ∀ (x : G), p (ConjAct.toConjAct x)
<VAR>G : Type u_3<VAR>DivInvMonoid G<GOAL>ConjAct.ofConjAct.symm = ConjAct.toConjAct
<VAR>G : Type u_3<VAR>DivInvMonoid G<GOAL>ConjAct.toConjAct.symm = ConjAct.ofConjAct
<VAR>G : Type u_3<VAR>DivInvMonoid G<VAR>x : ConjAct G<GOAL>ConjAct.toConjAct (ConjAct.ofConjAct x) = x
<VAR>G : Type u_3<VAR>DivInvMonoid G<VAR>x : G<GOAL>ConjAct.ofConjAct (ConjAct.toConjAct x) = x
<VAR>G : Type u_3<VAR>DivInvMonoid G<GOAL>ConjAct.ofConjAct 1 = 1
<VAR>G : Type u_3<VAR>DivInvMonoid G<GOAL>ConjAct.toConjAct 1 = 1
<VAR>G : Type u_3<VAR>DivInvMonoid G<VAR>x : ConjAct G<GOAL>ConjAct.ofConjAct x⁻¹ = (ConjAct.ofConjAct x)⁻¹
<VAR>G : Type u_3<VAR>DivInvMonoid G<VAR>x : G<GOAL>ConjAct.toConjAct x⁻¹ = (ConjAct.toConjAct x)⁻¹
<VAR>G : Type u_3<VAR>DivInvMonoid G<VAR>x y : ConjAct G<GOAL>ConjAct.ofConjAct (x * y) = ConjAct.ofConjAct x * ConjAct.ofConjAct y
<VAR>G : Type u_3<VAR>DivInvMonoid G<VAR>x y : G<GOAL>ConjAct.toConjAct (x * y) = ConjAct.toConjAct x * ConjAct.toConjAct y
<VAR>G : Type u_3<VAR>DivInvMonoid G<VAR>g : ConjAct G<VAR>h : G<GOAL>g • h = ConjAct.ofConjAct g * h * (ConjAct.ofConjAct g)⁻¹
<VAR>G : Type u_3<VAR>DivInvMonoid G<VAR>g h : G<GOAL>ConjAct.toConjAct g • h = g * h * g⁻¹
<VAR>M : Type u_2<VAR>Monoid M<VAR>g : ConjAct Mˣ<VAR>h : M<GOAL>g • h = ↑(ConjAct.ofConjAct g) * h * ↑(ConjAct.ofConjAct g)⁻¹
<VAR>G₀ : Type u_4<VAR>GroupWithZero G₀<GOAL>ConjAct.ofConjAct 0 = 0
<VAR>G₀ : Type u_4<VAR>GroupWithZero G₀<GOAL>ConjAct.toConjAct 0 = 0
<VAR>G : Type u_3<VAR>Group G<VAR>g : ConjAct G<VAR>h : G<GOAL>g • h = (MulAut.conj (ConjAct.ofConjAct g)) h
<VAR>G : Type u_3<VAR>Group G<GOAL>MulAction.fixedPoints (ConjAct G) G = ↑(Subgroup.center G)
<VAR>G : Type u_3<VAR>Group G<VAR>g h : G<GOAL>g ∈ MulAction.orbit (ConjAct G) h ↔ IsConj g h
<VAR>G : Type u_3<VAR>Group G<GOAL>(MulAction.orbitRel (ConjAct G) G).Rel = IsConj
<VAR>G : Type u_3<VAR>Group G<VAR>g : G<GOAL>MulAction.orbit (ConjAct G) g = (ConjClasses.mk g).carrier
<VAR>G : Type u_3<VAR>Group G<VAR>g : G<GOAL>MulAction.stabilizer (ConjAct G) g = Subgroup.centralizer ↑(Subgroup.zpowers (ConjAct.toConjAct g))
<VAR>G : Type u_3<VAR>Group G<VAR>H : Subgroup G<VAR>H.Normal<VAR>g : ConjAct G<VAR>h : ↥H<GOAL>↑(g • h) = g • ↑h
<VAR>G : Type u_3<VAR>Group G<VAR>H : Subgroup G<VAR>H.Normal<VAR>g : G<VAR>h : ↥H<GOAL>↑((MulAut.conjNormal g) h) = g * ↑h * g⁻¹
<VAR>G : Type u_3<VAR>Group G<VAR>H : Subgroup G<VAR>H.Normal<VAR>g : G<VAR>h : ↥H<GOAL>↑((MulEquiv.symm (MulAut.conjNormal g)) h) = g⁻¹ * ↑h * g
<VAR>G : Type u_3<VAR>Group G<VAR>H : Subgroup G<VAR>H.Normal<VAR>g : G<VAR>h : ↥H<GOAL>↑((MulAut.conjNormal g)⁻¹ h) = g⁻¹ * ↑h * g
<VAR>G : Type u_3<VAR>Group G<VAR>H : Subgroup G<VAR>H.Normal<VAR>h : ↥H<GOAL>MulAut.conjNormal ↑h = MulAut.conj h
<VAR>M : Type u_2<VAR>Monoid M<VAR>x : Mˣ<GOAL>∀ (a : ↥(MulAction.stabilizer (ConjAct Mˣ) x)), ↑↑((unitsCentralizerEquiv M x).symm a) = ↑(ConjAct.ofConjAct ↑a)
<VAR>M : Type u_2<VAR>Monoid M<VAR>x : Mˣ<GOAL>∀ (a : (↥(Submonoid.centralizer {↑x}))ˣ), ↑↑((unitsCentralizerEquiv M x) a) = ↑↑a
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>Monoid β<VAR>MulAction β α<VAR>H : Subgroup α<VAR>self : MulAction.QuotientAction β H<VAR>b : β<VAR>a a' : α<GOAL>a⁻¹ * a' ∈ H → (b • a)⁻¹ * b • a' ∈ H
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddMonoid β<VAR>AddAction β α<VAR>H : AddSubgroup α<VAR>self : AddAction.QuotientAction β H<VAR>b : β<VAR>a a' : α<GOAL>-a + a' ∈ H → -(b +ᵥ a) + (b +ᵥ a') ∈ H
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>Monoid β<VAR>MulAction β α<VAR>H : Subgroup α<VAR>MulAction.QuotientAction β H<VAR>b : β<VAR>a : α<GOAL>b • ↑a = ↑(b • a)
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddMonoid β<VAR>AddAction β α<VAR>H : AddSubgroup α<VAR>AddAction.QuotientAction β H<VAR>b : β<VAR>a : α<GOAL>b +ᵥ ↑a = ↑(b +ᵥ a)
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddMonoid β<VAR>AddAction β α<VAR>H : AddSubgroup α<VAR>AddAction.QuotientAction β H<VAR>b : β<VAR>q : α ⧸ H<GOAL>↑(b +ᵥ Quotient.out' q) = b +ᵥ q