mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Http.Server.Connection
/-- Injects a `Date` header into a response head if `Config.generateDate` is set
and the response does not already include one.
 -/
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.prepareResponseHead : Std.Http.Config → Std.Http.Response.Head → Std.Async.Async Std.Http.Response.Head
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- The orbits of infinite places under the action of the Galois group are indexed by
the infinite places of the base field.  -/
NumberField.InfinitePlace.orbitRelEquiv : {k : Type u_1} →
  [inst : Field k] →
    {K : Type u_2} →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] →
          [IsGalois k K] →
            Quotient (MulAction.orbitRel Gal(K/k) (NumberField.InfinitePlace K)) ≃ NumberField.InfinitePlace k
-- Mathlib.Algebra.Module.PID
Submodule.pOrder.congr_simp : ∀ {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst_1 : AddCommMonoid M] [inst_2 : DistribMulAction R M] {p p_1 : R}
  (e_p : p = p_1) (hM : Module.IsTorsion' M ↥(Submonoid.powers p)) (x x_1 : M),
  x = x_1 →
    ∀ {inst_3 : (n : ℕ) → Decidable (p ^ n • x = 0)} [inst_4 : (n : ℕ) → Decidable (p_1 ^ n • x_1 = 0)],
      Submodule.pOrder hM x = Submodule.pOrder ⋯ x_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.polynomialX_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R},
  W'.polynomialX =
    MvPolynomial.C W'.a₁ * MvPolynomial.X 1 * MvPolynomial.X 2 -
      (MvPolynomial.C 3 * MvPolynomial.X 0 ^ 2 + MvPolynomial.C (2 * W'.a₂) * MvPolynomial.X 0 * MvPolynomial.X 2 +
        MvPolynomial.C W'.a₄ * MvPolynomial.X 2 ^ 2)
-- Mathlib.FieldTheory.ChevalleyWarning
/-- The **Chevalley–Warning theorem**, finitary version.
Let `(f i)` be a finite family of multivariate polynomials
in finitely many variables (`X s`, `s : σ`) over a finite field of characteristic `p`.
Assume that the sum of the total degrees of the `f i` is less than the cardinality of `σ`.
Then the number of common solutions of the `f i` is divisible by `p`.  -/
char_dvd_card_solutions_of_sum_lt : ∀ {K : Type u_1} {σ : Type u_2} {ι : Type u_3} [inst : Fintype K] [inst_1 : Field K] [inst_2 : Fintype σ]
  [inst_3 : DecidableEq σ] [inst_4 : DecidableEq K] (p : ℕ) [CharP K p] {s : Finset ι} {f : ι → MvPolynomial σ K},
  ∑ i ∈ s, (f i).totalDegree < Fintype.card σ → p ∣ Fintype.card { x // ∀ i ∈ s, (MvPolynomial.eval x) (f i) = 0 }
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.linearIndependent_iff_sum : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  Profinite.NobelingProof.contained C (Order.succ o) →
    ∀ (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
      LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval C) ↔
        LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.SumEval C ho)