mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Matrix.Mul
Matrix.mul_sum : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : Fintype m] (s : Finset β) (f : β → Matrix m n α) (M : Matrix l m α), M * ∑ a ∈ s, f a = ∑ a ∈ s, M * f a
-- Lean.Parser.Term
Lean.Parser.Term.pipeProj.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_singleton_eq_self : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∉ s → s \ {a} = s
-- Mathlib.GroupTheory.PGroup
IsPGroup.to_sup_of_normal_right' : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H K : Subgroup G},
  IsPGroup p ↥H → IsPGroup p ↥K → H ≤ Subgroup.normalizer ↑K → IsPGroup p ↥(H ⊔ K)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.ncard_primesOver_of_prime_pow : ∀ (p k : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K],
  ((Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K)).ncard = 1