ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>S : Type u_3<VAR>Add S<VAR>a b : S<VAR>h : AddCommute a b<GOAL>AddSemiconjBy a b b
<VAR>S : Type u_3<VAR>Mul S<VAR>a b : S<GOAL>Commute a b ↔ Commute b a
<VAR>S : Type u_3<VAR>Add S<VAR>a b : S<GOAL>AddCommute a b ↔ AddCommute b a
<VAR>S : Type u_3<VAR>AddSemigroup S<VAR>a b c : S<VAR>hab : AddCommute a b<VAR>hac : AddCommute a c<GOAL>AddCommute a (b + c)
<VAR>S : Type u_3<VAR>Semigroup S<VAR>a b c : S<VAR>hab : Commute a b<VAR>hac : Commute a c<GOAL>Commute a (b * c)
<VAR>S : Type u_3<VAR>AddSemigroup S<VAR>a b c : S<VAR>hac : AddCommute a c<VAR>hbc : AddCommute b c<GOAL>AddCommute (a + b) c
<VAR>S : Type u_3<VAR>Semigroup S<VAR>a b c : S<VAR>hac : Commute a c<VAR>hbc : Commute b c<GOAL>Commute (a * b) c
<VAR>S : Type u_3<VAR>AddSemigroup S<VAR>b c : S<VAR>h : AddCommute b c<VAR>a : S<GOAL>a + b + c = a + c + b
<VAR>S : Type u_3<VAR>Semigroup S<VAR>b c : S<VAR>h : Commute b c<VAR>a : S<GOAL>a * b * c = a * c * b
<VAR>S : Type u_3<VAR>Semigroup S<VAR>a b : S<VAR>h : Commute a b<VAR>c : S<GOAL>a * (b * c) = b * (a * c)
<VAR>S : Type u_3<VAR>AddSemigroup S<VAR>a b : S<VAR>h : AddCommute a b<VAR>c : S<GOAL>a + (b + c) = b + (a + c)
<VAR>S : Type u_3<VAR>Semigroup S<VAR>b c : S<VAR>hbc : Commute b c<VAR>a d : S<GOAL>a * b * (c * d) = a * c * (b * d)
<VAR>S : Type u_3<VAR>AddSemigroup S<VAR>b c : S<VAR>hbc : AddCommute b c<VAR>a d : S<GOAL>a + b + (c + d) = a + c + (b + d)
<VAR>S : Type u_3<VAR>AddCommMagma S<VAR>a b : S<GOAL>AddCommute a b
<VAR>S : Type u_3<VAR>CommMagma S<VAR>a b : S<GOAL>Commute a b
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>a : M<GOAL>Commute a 1
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>a : M<GOAL>AddCommute a 0
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>a : M<GOAL>Commute 1 a
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>a : M<GOAL>AddCommute 0 a
<VAR>M : Type u_2<VAR>Monoid M<VAR>a b : M<VAR>h : Commute a b<VAR>n : ℕ<GOAL>Commute a (b ^ n)
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a b : M<VAR>h : AddCommute a b<VAR>n : ℕ<GOAL>AddCommute a (n • b)
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a b : M<VAR>h : AddCommute a b<VAR>n : ℕ<GOAL>AddCommute (n • a) b
<VAR>M : Type u_2<VAR>Monoid M<VAR>a b : M<VAR>h : Commute a b<VAR>n : ℕ<GOAL>Commute (a ^ n) b
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a b : M<VAR>h : AddCommute a b<VAR>m n : ℕ<GOAL>AddCommute (m • a) (n • b)
<VAR>M : Type u_2<VAR>Monoid M<VAR>a b : M<VAR>h : Commute a b<VAR>m n : ℕ<GOAL>Commute (a ^ m) (b ^ n)
<VAR>M : Type u_2<VAR>Monoid M<VAR>a : M<VAR>n : ℕ<GOAL>Commute a (a ^ n)
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a : M<VAR>n : ℕ<GOAL>AddCommute a (n • a)
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a : M<VAR>n : ℕ<GOAL>AddCommute (n • a) a
<VAR>M : Type u_2<VAR>Monoid M<VAR>a : M<VAR>n : ℕ<GOAL>Commute (a ^ n) a
<VAR>M : Type u_2<VAR>Monoid M<VAR>a : M<VAR>m n : ℕ<GOAL>Commute (a ^ m) (a ^ n)
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a : M<VAR>m n : ℕ<GOAL>AddCommute (m • a) (n • a)
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a b : M<VAR>h : AddCommute a b<VAR>n : ℕ<GOAL>n • (a + b) = n • a + n • b
<VAR>M : Type u_2<VAR>Monoid M<VAR>a b : M<VAR>h : Commute a b<VAR>n : ℕ<GOAL>(a * b) ^ n = a ^ n * b ^ n
<VAR>G : Type u_1<VAR>SubtractionMonoid G<VAR>a b : G<VAR>hab : AddCommute a b<GOAL>-(a + b) = -a + -b
<VAR>G : Type u_1<VAR>DivisionMonoid G<VAR>a b : G<VAR>hab : Commute a b<GOAL>(a * b)⁻¹ = a⁻¹ * b⁻¹
<VAR>G : Type u_1<VAR>SubtractionMonoid G<VAR>a b : G<VAR>h : AddCommute a b<VAR>n : ℤ<GOAL>n • (a + b) = n • a + n • b
<VAR>G : Type u_1<VAR>DivisionMonoid G<VAR>a b : G<VAR>h : Commute a b<VAR>n : ℤ<GOAL>(a * b) ^ n = a ^ n * b ^ n
<VAR>G : Type u_1<VAR>Group G<VAR>a b : G<VAR>h : Commute a b<GOAL>a * b * a⁻¹ = b
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a b : G<VAR>h : AddCommute a b<GOAL>a + b + -a = b
<VAR>G : Type u_1<VAR>Group G<VAR>a b : G<VAR>h : Commute a b<GOAL>a * (b * a⁻¹) = b
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a b : G<VAR>h : AddCommute a b<GOAL>a + (b + -a) = b
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>u : AddUnits M<GOAL>AddCommute a ↑u → AddCommute a ↑(-u)
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>u : Mˣ<GOAL>Commute a ↑u → Commute a ↑u⁻¹
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>u : Mˣ<GOAL>Commute a ↑u⁻¹ ↔ Commute a ↑u
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>u : AddUnits M<GOAL>AddCommute a ↑(-u) ↔ AddCommute a ↑u
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>u : Mˣ<GOAL>Commute (↑u) a → Commute (↑u⁻¹) a
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>u : AddUnits M<GOAL>AddCommute (↑u) a → AddCommute (↑(-u)) a
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>u : AddUnits M<GOAL>AddCommute (↑(-u)) a ↔ AddCommute (↑u) a
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>u : Mˣ<GOAL>Commute (↑u⁻¹) a ↔ Commute (↑u) a
<VAR>M : Type u_1<VAR>Monoid M<VAR>u₁ u₂ : Mˣ<GOAL>Commute u₁ u₂ → Commute ↑u₁ ↑u₂
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>u₁ u₂ : AddUnits M<GOAL>AddCommute u₁ u₂ → AddCommute ↑u₁ ↑u₂
<VAR>M : Type u_1<VAR>Monoid M<VAR>u₁ u₂ : Mˣ<GOAL>Commute ↑u₁ ↑u₂ → Commute u₁ u₂
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>u₁ u₂ : AddUnits M<GOAL>AddCommute ↑u₁ ↑u₂ → AddCommute u₁ u₂
<VAR>M : Type u_1<VAR>Monoid M<VAR>u₁ u₂ : Mˣ<GOAL>Commute ↑u₁ ↑u₂ ↔ Commute u₁ u₂
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>u₁ u₂ : AddUnits M<GOAL>AddCommute ↑u₁ ↑u₂ ↔ AddCommute u₁ u₂
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a b : M<VAR>h : AddCommute a b<GOAL>IsAddUnit (a + b) ↔ IsAddUnit a ∧ IsAddUnit b
<VAR>M : Type u_1<VAR>Monoid M<VAR>a b : M<VAR>h : Commute a b<GOAL>IsUnit (a * b) ↔ IsUnit a ∧ IsUnit b
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<GOAL>IsUnit (a * a) ↔ IsUnit a
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<GOAL>IsAddUnit (a + a) ↔ IsAddUnit a
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>u : Mˣ<VAR>h : Commute a ↑u<VAR>m : ℤ<GOAL>Commute a ↑(u ^ m)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>u : AddUnits M<VAR>h : AddCommute a ↑u<VAR>m : ℤ<GOAL>AddCommute a ↑(m • u)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>u : AddUnits M<VAR>h : AddCommute (↑u) a<VAR>m : ℤ<GOAL>AddCommute (↑(m • u)) a
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>u : Mˣ<VAR>h : Commute (↑u) a<VAR>m : ℤ<GOAL>Commute (↑(u ^ m)) a
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>n : ℕ<VAR>a : M<VAR>hn : n ≠ 0<GOAL>IsAddUnit (n • a) ↔ IsAddUnit a
<VAR>M : Type u_1<VAR>Monoid M<VAR>n : ℕ<VAR>a : M<VAR>hn : n ≠ 0<GOAL>IsUnit (a ^ n) ↔ IsUnit a
<VAR>M : Type u_1<VAR>Monoid M<VAR>n : ℕ<VAR>a : M<GOAL>IsUnit (a ^ (n + 1)) ↔ IsUnit a
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>n : ℕ<VAR>a : M<GOAL>IsAddUnit ((n + 1) • a) ↔ IsAddUnit a
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>n : ℕ<VAR>ha : a ^ n = 1<VAR>hn : n ≠ 0<GOAL>↑(Units.ofPowEqOne a n ha hn) = a
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>n : ℕ<VAR>ha : a ^ n = 1<VAR>hn : n ≠ 0<GOAL>↑(Units.ofPowEqOne a n ha hn)⁻¹ = a ^ (n - 1)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>n : ℕ<VAR>ha : n • a = 0<VAR>hn : n ≠ 0<GOAL>↑(AddUnits.ofNSMulEqZero a n ha hn) = a
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>n : ℕ<VAR>ha : n • a = 0<VAR>hn : n ≠ 0<GOAL>↑(-AddUnits.ofNSMulEqZero a n ha hn) = (n - 1) • a
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>n : ℕ<VAR>a : M<VAR>ha : n • a = 0<VAR>hn : n ≠ 0<GOAL>n • AddUnits.ofNSMulEqZero a n ha hn = 0
<VAR>M : Type u_1<VAR>Monoid M<VAR>n : ℕ<VAR>a : M<VAR>ha : a ^ n = 1<VAR>hn : n ≠ 0<GOAL>Units.ofPowEqOne a n ha hn ^ n = 1
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>n : ℕ<VAR>a : M<VAR>ha : n • a = 0<VAR>hn : n ≠ 0<GOAL>IsAddUnit a
<VAR>M : Type u_1<VAR>Monoid M<VAR>n : ℕ<VAR>a : M<VAR>ha : a ^ n = 1<VAR>hn : n ≠ 0<GOAL>IsUnit a
<VAR>M : Type u_1<VAR>DivisionMonoid M<VAR>a b c d : M<VAR>hbd : Commute b d<VAR>hb : IsUnit b<VAR>hd : IsUnit d<GOAL>a / b = c / d ↔ a * d = c * b
<VAR>M : Type u_1<VAR>SubtractionMonoid M<VAR>a b c d : M<VAR>hbd : AddCommute b d<VAR>hb : IsAddUnit b<VAR>hd : IsAddUnit d<GOAL>a - b = c - d ↔ a + d = c + b
<VAR>M : Type u_1<VAR>α : Type u_4<VAR>β : Type u_5<VAR>VAdd M α<VAR>VAdd M β<VAR>a : M<VAR>x : α ⊕ β<GOAL>a +ᵥ x = Sum.map (fun x => a +ᵥ x) (fun x => a +ᵥ x) x
<VAR>M : Type u_1<VAR>α : Type u_4<VAR>β : Type u_5<VAR>SMul M α<VAR>SMul M β<VAR>a : M<VAR>x : α ⊕ β<GOAL>a • x = Sum.map (fun x => a • x) (fun x => a • x) x
<VAR>M : Type u_1<VAR>α : Type u_4<VAR>β : Type u_5<VAR>VAdd M α<VAR>VAdd M β<VAR>a : M<VAR>b : α<GOAL>a +ᵥ Sum.inl b = Sum.inl (a +ᵥ b)
<VAR>M : Type u_1<VAR>α : Type u_4<VAR>β : Type u_5<VAR>SMul M α<VAR>SMul M β<VAR>a : M<VAR>b : α<GOAL>a • Sum.inl b = Sum.inl (a • b)
<VAR>M : Type u_1<VAR>α : Type u_4<VAR>β : Type u_5<VAR>VAdd M α<VAR>VAdd M β<VAR>a : M<VAR>c : β<GOAL>a +ᵥ Sum.inr c = Sum.inr (a +ᵥ c)
<VAR>M : Type u_1<VAR>α : Type u_4<VAR>β : Type u_5<VAR>SMul M α<VAR>SMul M β<VAR>a : M<VAR>c : β<GOAL>a • Sum.inr c = Sum.inr (a • c)
<VAR>M : Type u_1<VAR>α : Type u_4<VAR>β : Type u_5<VAR>SMul M α<VAR>SMul M β<VAR>a : M<VAR>x : α ⊕ β<GOAL>(a • x).swap = a • x.swap
<VAR>M : Type u_1<VAR>α : Type u_4<VAR>β : Type u_5<VAR>VAdd M α<VAR>VAdd M β<VAR>a : M<VAR>x : α ⊕ β<GOAL>(a +ᵥ x).swap = a +ᵥ x.swap
<VAR>M : Type u_3<VAR>α : Type u_5<VAR>AddMonoid M<VAR>VAdd M α<VAR>m : AddUnits M<VAR>a : α<GOAL>m +ᵥ a = ↑m +ᵥ a
<VAR>M : Type u_3<VAR>α : Type u_5<VAR>Monoid M<VAR>SMul M α<VAR>m : Mˣ<VAR>a : α<GOAL>m • a = ↑m • a
<VAR>M : Type u_6<VAR>α : Type u_7<VAR>AddMonoid M<VAR>VAdd M α<VAR>m n : M<VAR>h₁ : m + n = 0<VAR>h₂ : n + m = 0<VAR>a : α<GOAL>{ val := m, neg := n, val_neg := h₁, neg_val := h₂ } +ᵥ a = m +ᵥ a
<VAR>M : Type u_6<VAR>α : Type u_7<VAR>Monoid M<VAR>SMul M α<VAR>m n : M<VAR>h₁ : m * n = 1<VAR>h₂ : n * m = 1<VAR>a : α<GOAL>{ val := m, inv := n, val_inv := h₁, inv_val := h₂ } • a = m • a
<VAR>M : Type u_3<VAR>α : Type u_5<VAR>Monoid M<VAR>SMul M α<VAR>m : M<VAR>hm : IsUnit m<VAR>a : α<GOAL>hm.unit • a = m • a
<VAR>α : Type u_5<VAR>AddMonoid α<VAR>a : α<VAR>h : IsAddUnit a<GOAL>-h.addUnit +ᵥ a = 0
<VAR>α : Type u_5<VAR>Monoid α<VAR>a : α<VAR>h : IsUnit a<GOAL>h.unit⁻¹ • a = 1
<VAR>G : Type u_1<VAR>M : Type u_3<VAR>Group G<VAR>Monoid M<VAR>MulAction G M<VAR>SMulCommClass G M M<VAR>IsScalarTower G M M<VAR>g : G<VAR>m : Mˣ<GOAL>↑(g • m) = g • ↑m
<VAR>G : Type u_1<VAR>M : Type u_3<VAR>AddGroup G<VAR>AddMonoid M<VAR>AddAction G M<VAR>VAddCommClass G M M<VAR>VAddAssocClass G M M<VAR>g : G<VAR>m : AddUnits M<GOAL>↑(g +ᵥ m) = g +ᵥ ↑m
<VAR>G : Type u_1<VAR>M : Type u_3<VAR>Group G<VAR>Monoid M<VAR>MulAction G M<VAR>SMulCommClass G M M<VAR>IsScalarTower G M M<VAR>g : G<VAR>m : Mˣ<GOAL>(g • m)⁻¹ = g⁻¹ • m⁻¹
<VAR>G : Type u_1<VAR>M : Type u_3<VAR>AddGroup G<VAR>AddMonoid M<VAR>AddAction G M<VAR>VAddCommClass G M M<VAR>VAddAssocClass G M M<VAR>g : G<VAR>m : AddUnits M<GOAL>-(g +ᵥ m) = -g +ᵥ -m
<VAR>G : Type u_1<VAR>M : Type u_3<VAR>Group G<VAR>Monoid M<VAR>MulAction G M<VAR>SMulCommClass G M M<VAR>IsScalarTower G M M<VAR>m : M<VAR>g : G<VAR>h : IsUnit m<GOAL>IsUnit (g • m)
<VAR>G : Type u_1<VAR>M : Type u_3<VAR>AddGroup G<VAR>AddMonoid M<VAR>AddAction G M<VAR>VAddCommClass G M M<VAR>VAddAssocClass G M M<VAR>m : M<VAR>g : G<VAR>h : IsAddUnit m<GOAL>IsAddUnit (g +ᵥ m)
<VAR>M : Type u<VAR>m₁ m₂ : AddMonoid M<VAR>h_mul : HAdd.hAdd = HAdd.hAdd<GOAL>m₁ = m₂
<VAR>M : Type u<GOAL>Function.Injective (@AddCommMonoid.toAddMonoid M)
<VAR>M : Type u<GOAL>Function.Injective (@CommMonoid.toMonoid M)
<VAR>M : Type u_1<VAR>m₁ m₂ : CommMonoid M<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>m₁ = m₂
<VAR>M : Type u_1<VAR>m₁ m₂ : AddCommMonoid M<VAR>h_mul : HAdd.hAdd = HAdd.hAdd<GOAL>m₁ = m₂
<VAR>M : Type u<GOAL>Function.Injective (@AddLeftCancelMonoid.toAddMonoid M)
<VAR>M : Type u<GOAL>Function.Injective (@LeftCancelMonoid.toMonoid M)
<VAR>M : Type u<VAR>m₁ m₂ : LeftCancelMonoid M<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>m₁ = m₂
<VAR>M : Type u<VAR>m₁ m₂ : AddLeftCancelMonoid M<VAR>h_mul : HAdd.hAdd = HAdd.hAdd<GOAL>m₁ = m₂
<VAR>M : Type u<GOAL>Function.Injective (@AddRightCancelMonoid.toAddMonoid M)
<VAR>M : Type u<GOAL>Function.Injective (@RightCancelMonoid.toMonoid M)
<VAR>M : Type u<VAR>m₁ m₂ : RightCancelMonoid M<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>m₁ = m₂
<VAR>M : Type u<VAR>m₁ m₂ : AddRightCancelMonoid M<VAR>h_mul : HAdd.hAdd = HAdd.hAdd<GOAL>m₁ = m₂
<VAR>M : Type u<GOAL>Function.Injective (@AddCancelMonoid.toAddLeftCancelMonoid M)
<VAR>M : Type u<GOAL>Function.Injective (@CancelMonoid.toLeftCancelMonoid M)
<VAR>M : Type u_1<VAR>m₁ m₂ : AddCancelMonoid M<VAR>h_mul : HAdd.hAdd = HAdd.hAdd<GOAL>m₁ = m₂
<VAR>M : Type u_1<VAR>m₁ m₂ : CancelMonoid M<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>m₁ = m₂
<VAR>M : Type u<GOAL>Function.Injective (@CancelCommMonoid.toCommMonoid M)
<VAR>M : Type u<GOAL>Function.Injective (@AddCancelCommMonoid.toAddCommMonoid M)
<VAR>M : Type u_1<VAR>m₁ m₂ : CancelCommMonoid M<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>m₁ = m₂
<VAR>M : Type u_1<VAR>m₁ m₂ : AddCancelCommMonoid M<VAR>h_mul : HAdd.hAdd = HAdd.hAdd<GOAL>m₁ = m₂
<VAR>M : Type u_1<VAR>m₁ m₂ : SubNegMonoid M<VAR>h_mul : HAdd.hAdd = HAdd.hAdd<VAR>h_inv : Neg.neg = Neg.neg<GOAL>m₁ = m₂
<VAR>G : Type u_1<GOAL>Function.Injective (@AddGroup.toSubNegMonoid G)
<VAR>G : Type u_1<GOAL>Function.Injective (@Group.toDivInvMonoid G)
<VAR>G : Type u_1<VAR>g₁ g₂ : Group G<VAR>h_mul : Mul.mul = Mul.mul<GOAL>g₁ = g₂
<VAR>G : Type u_1<VAR>g₁ g₂ : AddGroup G<VAR>h_mul : Add.add = Add.add<GOAL>g₁ = g₂
<VAR>G : Type u_1<GOAL>Function.Injective (@AddCommGroup.toAddGroup G)
<VAR>G : Type u_1<GOAL>Function.Injective (@CommGroup.toGroup G)
<VAR>G : Type u_1<VAR>g₁ g₂ : AddCommGroup G<VAR>h_mul : Add.add = Add.add<GOAL>g₁ = g₂
<VAR>G : Type u_1<VAR>g₁ g₂ : CommGroup G<VAR>h_mul : Mul.mul = Mul.mul<GOAL>g₁ = g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Group α<VAR>MulAction α β<VAR>a : α<VAR>x : β<GOAL>(MulAction.toPerm a) x = a • x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Group α<VAR>MulAction α β<VAR>a : α<VAR>x : β<GOAL>(Equiv.symm (MulAction.toPerm a)) x = a⁻¹ • x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddGroup α<VAR>AddAction α β<VAR>a : α<VAR>x : β<GOAL>(AddAction.toPerm a) x = a +ᵥ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddGroup α<VAR>AddAction α β<VAR>a : α<VAR>x : β<GOAL>(Equiv.symm (AddAction.toPerm a)) x = -a +ᵥ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Group α<VAR>MulAction α β<VAR>FaithfulSMul α β<GOAL>Function.Injective MulAction.toPerm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddGroup α<VAR>AddAction α β<VAR>FaithfulVAdd α β<GOAL>Function.Injective AddAction.toPerm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Group α<VAR>MulAction α β<VAR>a : α<GOAL>(MulAction.toPermHom α β) a = MulAction.toPerm a
<VAR>β : Type u_2<VAR>α : Type u_4<VAR>AddGroup α<VAR>AddAction α β<VAR>a : α<VAR>x : β<GOAL>(Equiv.symm ((AddAction.toPermHom β α) a)) x = (Multiplicative.ofAdd a)⁻¹ • x
<VAR>β : Type u_2<VAR>α : Type u_4<VAR>AddGroup α<VAR>AddAction α β<VAR>a : α<VAR>x : β<GOAL>((AddAction.toPermHom β α) a) x = a +ᵥ x
<VAR>α : Type u_4<VAR>f : Equiv.Perm α<VAR>a : α<GOAL>f • a = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Group α<VAR>MulAction α β<VAR>g : α<GOAL>Function.Bijective fun x => g • x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddGroup α<VAR>AddAction α β<VAR>g : α<GOAL>Function.Bijective fun x => g +ᵥ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddGroup α<VAR>AddAction α β<VAR>g : α<GOAL>Function.Injective fun x => g +ᵥ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Group α<VAR>MulAction α β<VAR>g : α<GOAL>Function.Injective fun x => g • x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Group α<VAR>MulAction α β<VAR>g : α<GOAL>Function.Surjective fun x => g • x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddGroup α<VAR>AddAction α β<VAR>g : α<GOAL>Function.Surjective fun x => g +ᵥ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddGroup α<VAR>AddAction α β<VAR>g : α<VAR>x y : β<VAR>h : g +ᵥ x = g +ᵥ y<GOAL>x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Group α<VAR>MulAction α β<VAR>g : α<VAR>x y : β<VAR>h : g • x = g • y<GOAL>x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Group α<VAR>MulAction α β<VAR>g : α<VAR>x y : β<GOAL>g • x = g • y ↔ x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddGroup α<VAR>AddAction α β<VAR>g : α<VAR>x y : β<GOAL>g +ᵥ x = g +ᵥ y ↔ x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddGroup α<VAR>AddAction α β<VAR>g : α<VAR>x y : β<GOAL>g +ᵥ x = y ↔ x = -g +ᵥ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Group α<VAR>MulAction α β<VAR>g : α<VAR>x y : β<GOAL>g • x = y ↔ x = g⁻¹ • y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Monoid α<VAR>MulAction α β<VAR>c : α<VAR>x : β<VAR>Invertible c<GOAL>⅟c • c • x = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Monoid α<VAR>MulAction α β<VAR>c : α<VAR>x : β<VAR>Invertible c<GOAL>c • ⅟c • x = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Monoid α<VAR>MulAction α β<VAR>c : α<VAR>x y : β<VAR>Invertible c<GOAL>⅟c • x = y ↔ x = c • y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Monoid α<VAR>MulAction α β<VAR>c : α<VAR>x y : β<VAR>Invertible c<GOAL>c • x = y ↔ x = ⅟c • y
<VAR>G : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>SubtractionMonoid G<VAR>AddAction G A<VAR>g : G<VAR>F : A → B<VAR>a : A<GOAL>VAdd.vadd g F a = F (-g +ᵥ a)
<VAR>G : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>DivisionMonoid G<VAR>MulAction G A<VAR>g : G<VAR>F : A → B<VAR>a : A<GOAL>SMul.smul g F a = F (g⁻¹ • a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddMonoid α<VAR>AddAction α β<VAR>a : α<VAR>ha : IsAddUnit a<VAR>x y : β<GOAL>a +ᵥ x = a +ᵥ y ↔ x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Monoid α<VAR>MulAction α β<VAR>a : α<VAR>ha : IsUnit a<VAR>x y : β<GOAL>a • x = a • y ↔ x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Group α<VAR>Monoid β<VAR>MulAction α β<VAR>SMulCommClass α β β<VAR>IsScalarTower α β β<VAR>g : α<VAR>m : β<GOAL>IsUnit (g • m) ↔ IsUnit m
<VAR>M : Type u_2<VAR>α : Type u_4<VAR>SMul M α<VAR>SMul Mᵐᵒᵖ α<VAR>IsCentralScalar M α<VAR>r : M<VAR>a : α<GOAL>MulOpposite.op (r • a) = MulOpposite.op r • MulOpposite.op a
<VAR>M : Type u_2<VAR>α : Type u_4<VAR>VAdd M α<VAR>VAdd Mᵃᵒᵖ α<VAR>IsCentralVAdd M α<VAR>r : M<VAR>a : α<GOAL>AddOpposite.op (r +ᵥ a) = AddOpposite.op r +ᵥ AddOpposite.op a
<VAR>M : Type u_2<VAR>α : Type u_4<VAR>SMul M α<VAR>SMul Mᵐᵒᵖ α<VAR>IsCentralScalar M α<VAR>r : Mᵐᵒᵖ<VAR>a : αᵐᵒᵖ<GOAL>MulOpposite.unop (r • a) = MulOpposite.unop r • MulOpposite.unop a
<VAR>M : Type u_2<VAR>α : Type u_4<VAR>VAdd M α<VAR>VAdd Mᵃᵒᵖ α<VAR>IsCentralVAdd M α<VAR>r : Mᵃᵒᵖ<VAR>a : αᵃᵒᵖ<GOAL>AddOpposite.unop (r +ᵥ a) = AddOpposite.unop r +ᵥ AddOpposite.unop a
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>Monoid α<VAR>MulAction αᵐᵒᵖ β<VAR>b : β<VAR>a₁ a₂ : α<GOAL>MulOpposite.op a₂ • MulOpposite.op a₁ • b = MulOpposite.op (a₁ * a₂) • b
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>AddMonoid α<VAR>AddAction αᵃᵒᵖ β<VAR>b : β<VAR>a₁ a₂ : α<GOAL>AddOpposite.op a₂ +ᵥ (AddOpposite.op a₁ +ᵥ b) = AddOpposite.op (a₁ + a₂) +ᵥ b
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>AddMonoid α<VAR>AddAction αᵃᵒᵖ β<VAR>b : β<VAR>a₁ a₂ : α<GOAL>AddOpposite.op (a₁ + a₂) +ᵥ b = AddOpposite.op a₂ +ᵥ (AddOpposite.op a₁ +ᵥ b)
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>Monoid α<VAR>MulAction αᵐᵒᵖ β<VAR>b : β<VAR>a₁ a₂ : α<GOAL>MulOpposite.op (a₁ * a₂) • b = MulOpposite.op a₂ • MulOpposite.op a₁ • b
<VAR>α : Type u_4<VAR>Mul α<VAR>a a' : α<GOAL>MulOpposite.op a • a' = a' * a
<VAR>α : Type u_4<VAR>Add α<VAR>a a' : α<GOAL>AddOpposite.op a +ᵥ a' = a' + a
<VAR>α : Type u_4<VAR>Mul α<VAR>a : αᵐᵒᵖ<VAR>a' : α<GOAL>a • a' = a' * MulOpposite.unop a
<VAR>α : Type u_4<VAR>Add α<VAR>a : αᵃᵒᵖ<VAR>a' : α<GOAL>a +ᵥ a' = a' + AddOpposite.unop a
<VAR>ι : Type u_1<VAR>α : ι → Type u_4<VAR>β : ι → Type u_5<VAR>i : ι<VAR>(i : ι) → SMul (α i) (β i)<VAR>s : (i : ι) → α i<VAR>x : (i : ι) → β i<GOAL>(s • x) i = s i • x i
<VAR>ι : Type u_1<VAR>α : ι → Type u_4<VAR>β : ι → Type u_5<VAR>i : ι<VAR>(i : ι) → VAdd (α i) (β i)<VAR>s : (i : ι) → α i<VAR>x : (i : ι) → β i<GOAL>(s +ᵥ x) i = s i +ᵥ x i
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>α : ι → Type u_4<VAR>(i : ι) → SMul M (α i)<VAR>∀ (i : ι), Nonempty (α i)<VAR>i : ι<VAR>FaithfulSMul M (α i)<GOAL>FaithfulSMul M ((i : ι) → α i)
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>α : ι → Type u_4<VAR>(i : ι) → VAdd M (α i)<VAR>∀ (i : ι), Nonempty (α i)<VAR>i : ι<VAR>FaithfulVAdd M (α i)<GOAL>FaithfulVAdd M ((i : ι) → α i)
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>α : ι → Type u_4<VAR>(i : ι) → SMul M (α i)<VAR>DecidableEq ι<VAR>c : M<VAR>f₁ : (i : ι) → α i<VAR>i : ι<VAR>x₁ : α i<GOAL>Function.update (c • f₁) i (c • x₁) = c • Function.update f₁ i x₁
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>α : ι → Type u_4<VAR>(i : ι) → VAdd M (α i)<VAR>DecidableEq ι<VAR>c : M<VAR>f₁ : (i : ι) → α i<VAR>i : ι<VAR>x₁ : α i<GOAL>Function.update (c +ᵥ f₁) i (c +ᵥ x₁) = c +ᵥ Function.update f₁ i x₁
<VAR>ι : Type u_1<VAR>M : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>VAdd M β<VAR>r : M<VAR>f : ι → α<VAR>g : ι → β<VAR>e : α → β<GOAL>Function.extend f (r +ᵥ g) (r +ᵥ e) = r +ᵥ Function.extend f g e
<VAR>ι : Type u_1<VAR>M : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>SMul M β<VAR>r : M<VAR>f : ι → α<VAR>g : ι → β<VAR>e : α → β<GOAL>Function.extend f (r • g) (r • e) = r • Function.extend f g e
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>α : ι → Type u_4<VAR>(i : ι) → SMul M (α i)<VAR>s : Set ι<VAR>(i : ι) → Decidable (i ∈ s)<VAR>c : M<VAR>f₁ g₁ : (i : ι) → α i<GOAL>s.piecewise (c • f₁) (c • g₁) = c • s.piecewise f₁ g₁
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>α : ι → Type u_4<VAR>(i : ι) → VAdd M (α i)<VAR>s : Set ι<VAR>(i : ι) → Decidable (i ∈ s)<VAR>c : M<VAR>f₁ g₁ : (i : ι) → α i<GOAL>s.piecewise (c +ᵥ f₁) (c +ᵥ g₁) = c +ᵥ s.piecewise f₁ g₁
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>SMul M α<VAR>a : M<VAR>x : Option α<GOAL>a • x = Option.map (fun x => a • x) x
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>VAdd M α<VAR>a : M<VAR>x : Option α<GOAL>a +ᵥ x = Option.map (fun x => a +ᵥ x) x
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>SMul M α<VAR>a : M<GOAL>a • none = none
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>VAdd M α<VAR>a : M<GOAL>a +ᵥ none = none
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>VAdd M α<VAR>a : M<VAR>b : α<GOAL>a +ᵥ some b = some (a +ᵥ b)
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>SMul M α<VAR>a : M<VAR>b : α<GOAL>a • some b = some (a • b)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : AddSubgroup G<VAR>l : List G<GOAL>(∀ x ∈ l, x ∈ K) → l.sum ∈ K
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>l : List G<GOAL>(∀ x ∈ l, x ∈ K) → l.prod ∈ K
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>K : AddSubgroup G<VAR>g : Multiset G<GOAL>(∀ a ∈ g, a ∈ K) → g.sum ∈ K
<VAR>G : Type u_3<VAR>CommGroup G<VAR>K : Subgroup G<VAR>g : Multiset G<GOAL>(∀ a ∈ g, a ∈ K) → g.prod ∈ K
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>g : Multiset G<VAR>comm : {x | x ∈ g}.Pairwise Commute<GOAL>(∀ a ∈ g, a ∈ K) → g.noncommProd comm ∈ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : AddSubgroup G<VAR>g : Multiset G<VAR>comm : {x | x ∈ g}.Pairwise AddCommute<GOAL>(∀ a ∈ g, a ∈ K) → g.noncommSum comm ∈ K
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>K : AddSubgroup G<VAR>ι : Type u_4<VAR>t : Finset ι<VAR>f : ι → G<VAR>h : ∀ c ∈ t, f c ∈ K<GOAL>∑ c ∈ t, f c ∈ K
<VAR>G : Type u_3<VAR>CommGroup G<VAR>K : Subgroup G<VAR>ι : Type u_4<VAR>t : Finset ι<VAR>f : ι → G<VAR>h : ∀ c ∈ t, f c ∈ K<GOAL>∏ c ∈ t, f c ∈ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : AddSubgroup G<VAR>ι : Type u_3<VAR>t : Finset ι<VAR>f : ι → G<VAR>comm : (↑t).Pairwise fun a b => AddCommute (f a) (f b)<GOAL>(∀ c ∈ t, f c ∈ K) → t.noncommSum f comm ∈ K
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>ι : Type u_3<VAR>t : Finset ι<VAR>f : ι → G<VAR>comm : (↑t).Pairwise fun a b => Commute (f a) (f b)<GOAL>(∀ c ∈ t, f c ∈ K) → t.noncommProd f comm ∈ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>l : List ↥H<GOAL>↑l.sum = (List.map Subtype.val l).sum
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>l : List ↥H<GOAL>↑l.prod = (List.map Subtype.val l).prod
<VAR>G : Type u_3<VAR>CommGroup G<VAR>H : Subgroup G<VAR>m : Multiset ↥H<GOAL>↑m.prod = (Multiset.map Subtype.val m).prod
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>H : AddSubgroup G<VAR>m : Multiset ↥H<GOAL>↑m.sum = (Multiset.map Subtype.val m).sum
<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>AddCommGroup G<VAR>H : AddSubgroup G<VAR>f : ι → ↥H<VAR>s : Finset ι<GOAL>↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>CommGroup G<VAR>H : Subgroup G<VAR>f : ι → ↥H<VAR>s : Finset ι<GOAL>↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>Nat.card ↥⊥ = 1
<VAR>G : Type u_1<VAR>Group G<GOAL>Nat.card ↥⊥ = 1
<VAR>G : Type u_1<VAR>Group G<GOAL>Nat.card ↥⊤ = Nat.card G
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>Nat.card ↥⊤ = Nat.card G
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>Finite ↥H<VAR>h : Nat.card ↥H = Nat.card G<GOAL>H = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>Finite ↥H<VAR>h : Nat.card ↥H = Nat.card G<GOAL>H = ⊤