Loogle!

Result

Found 139 declarations mentioning Polynomial.comp.

• Polynomial.comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] (p q : Polynomial R) : Polynomial R
• Polynomial.X_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.X.comp p = p
• Polynomial.comp_X 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : p.comp Polynomial.X = p
• Polynomial.natCast_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : (↑n).comp p = ↑n
• Polynomial.one_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.comp 1 p = 1
• Polynomial.zero_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.comp 0 p = 0
• Polynomial.ofNat_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).comp p = ↑n
• Polynomial.intCast_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Ring R] {p : Polynomial R} (i : ℤ) : (↑i).comp p = ↑i
• Polynomial.isRoot_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u_1} [CommSemiring R] {p q : Polynomial R} {r : R} : (p.comp q).IsRoot r ↔ p.IsRoot (Polynomial.eval r q)
• Polynomial.eval_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [CommSemiring R] {p q : Polynomial R} {x : R} : Polynomial.eval x (p.comp q) = Polynomial.eval (Polynomial.eval x q) p
• Polynomial.comp_assoc 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u_1} [CommSemiring R] (φ ψ χ : Polynomial R) : (φ.comp ψ).comp χ = φ.comp (ψ.comp χ)
• Polynomial.neg_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Ring R] {p q : Polynomial R} : (-p).comp q = -p.comp q
• Polynomial.map_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (p q : Polynomial R) : Polynomial.map f (p.comp q) = (Polynomial.map f p).comp (Polynomial.map f q)
• Polynomial.sum_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {ι : Type y} [Semiring R] (s : Finset ι) (p : ι → Polynomial R) (q : Polynomial R) : (∑ i ∈ s, p i).comp q = ∑ i ∈ s, (p i).comp q
• Polynomial.mul_X_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p r : Polynomial R} : (p * Polynomial.X).comp r = p.comp r * r
• Polynomial.add_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p q r : Polynomial R} : (p + q).comp r = p.comp r + q.comp r
• Polynomial.natCast_mul_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p r : Polynomial R} {n : ℕ} : (↑n * p).comp r = ↑n * p.comp r
• Polynomial.prod_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [CommSemiring R] {ι : Type u_1} (s : Finset ι) (p : ι → Polynomial R) (q : Polynomial R) : (∏ j ∈ s, p j).comp q = ∏ j ∈ s, (p j).comp q
• Polynomial.X_pow_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {k : ℕ} : (Polynomial.X ^ k).comp p = p ^ k
• Polynomial.comp_zero 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : p.comp 0 = Polynomial.C (Polynomial.eval 0 p)
• Polynomial.multiset_prod_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [CommSemiring R] (s : Multiset (Polynomial R)) (q : Polynomial R) : s.prod.comp q = (Multiset.map (fun p => p.comp q) s).prod
• Polynomial.comp_one 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : p.comp 1 = Polynomial.C (Polynomial.eval 1 p)
• Polynomial.list_prod_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [CommSemiring R] (l : List (Polynomial R)) (q : Polynomial R) : l.prod.comp q = (List.map (fun p => p.comp q) l).prod
• Polynomial.C_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} : (Polynomial.C a).comp p = Polynomial.C a
• Polynomial.sub_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Ring R] {p q r : Polynomial R} : (p - q).comp r = p.comp r - q.comp r
• Polynomial.comp_C 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} : p.comp (Polynomial.C a) = Polynomial.C (Polynomial.eval a p)
• Polynomial.mul_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u_1} [CommSemiring R] (p q r : Polynomial R) : (p * q).comp r = p.comp r * q.comp r
• Polynomial.mul_X_add_natCast_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p q : Polynomial R} {n : ℕ} : (p * (Polynomial.X + ↑n)).comp q = p.comp q * (q + ↑n)
• Polynomial.coe_compRingHom_apply 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [CommSemiring R] (p q : Polynomial R) : q.compRingHom p = p.comp q
• Polynomial.coe_compRingHom 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [CommSemiring R] (q : Polynomial R) : ⇑q.compRingHom = fun p => p.comp q
• Polynomial.mul_X_pow_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p r : Polynomial R} {k : ℕ} : (p * Polynomial.X ^ k).comp r = p.comp r * r ^ k
• Polynomial.pow_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u_1} [CommSemiring R] (p q : Polynomial R) (n : ℕ) : (p ^ n).comp q = p.comp q ^ n
• Polynomial.comp_eq_sum_left 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p q : Polynomial R} : p.comp q = p.sum fun e a => Polynomial.C a * q ^ e
• Polynomial.mul_comp_neg_X 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u_1} [Ring R] (p q : Polynomial R) : (p * q).comp (-Polynomial.X) = p.comp (-Polynomial.X) * q.comp (-Polynomial.X)
• Polynomial.C_mul_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a : R} [Semiring R] {p r : Polynomial R} : (Polynomial.C a * p).comp r = Polynomial.C a * p.comp r
• Polynomial.mul_X_sub_intCast_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Ring R] {p q : Polynomial R} {n : ℕ} : (p * (Polynomial.X - ↑n)).comp q = p.comp q * (q - ↑n)
• Polynomial.monomial_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (n : ℕ) : ((Polynomial.monomial n) a).comp p = Polynomial.C a * p ^ n
• Polynomial.eval₂_comp' 📋 Mathlib.Algebra.Polynomial.Eval.Algebra
  {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (x : S) (p q : Polynomial R) : Polynomial.eval₂ (algebraMap R S) x (p.comp q) = Polynomial.eval₂ (algebraMap R S) (Polynomial.eval₂ (algebraMap R S) x q) p
• Polynomial.iterate_comp_eval 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} [CommSemiring R] {p q : Polynomial R} (k : ℕ) (t : R) : Polynomial.eval t (p.comp^[k] q) = (fun x => Polynomial.eval x p)^[k] (Polynomial.eval t q)
• Polynomial.eval₂_comp 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] {p q : Polynomial R} [CommSemiring S] (f : R →+* S) {x : S} : Polynomial.eval₂ f x (p.comp q) = Polynomial.eval₂ f (Polynomial.eval₂ f x q) p
• Polynomial.iterate_comp_eval₂ 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] {p q : Polynomial R} [CommSemiring S] (f : R →+* S) (k : ℕ) (t : S) : Polynomial.eval₂ f t (p.comp^[k] q) = (fun x => Polynomial.eval₂ f x p)^[k] (Polynomial.eval₂ f t q)
• Polynomial.coeff_comp_degree_mul_degree 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} [Semiring R] {p q : Polynomial R} (hqd0 : q.natDegree ≠ 0) : (p.comp q).coeff (p.natDegree * q.natDegree) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
• Polynomial.comp_C_mul_X_eq_zero_iff 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} [Semiring R] {p : Polynomial R} {r : R} (hr : r ∈ nonZeroDivisors R) : p.comp (Polynomial.C r * Polynomial.X) = 0 ↔ p = 0
• Polynomial.comp_C_mul_X_coeff 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} [Semiring R] {p : Polynomial R} {r : R} {n : ℕ} : (p.comp (Polynomial.C r * Polynomial.X)).coeff n = p.coeff n * r ^ n
• Polynomial.comp_neg_X_comp_neg_X 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u_3} [CommRing R] (p : Polynomial R) : (p.comp (-Polynomial.X)).comp (-Polynomial.X) = p
• Polynomial.algEquivOfCompEqX 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] (p q : Polynomial R) (hpq : p.comp q = Polynomial.X) (hqp : q.comp p = Polynomial.X) : Polynomial R ≃ₐ[R] Polynomial R
• Polynomial.comp_X_add_C_eq_zero_iff 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {S : Type v} [Semiring S] {p : Polynomial S} {t : S} : p.comp (Polynomial.X + Polynomial.C t) = 0 ↔ p = 0
• Polynomial.comp_X_add_C_ne_zero_iff 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {S : Type v} [Semiring S] {p : Polynomial S} {t : S} : p.comp (Polynomial.X + Polynomial.C t) ≠ 0 ↔ p ≠ 0
• Polynomial.algEquivOfCompEqX_symm 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] (p q : Polynomial R) (hpq : p.comp q = Polynomial.X) (hqp : q.comp p = Polynomial.X) : (p.algEquivOfCompEqX q hpq hqp).symm = q.algEquivOfCompEqX p hqp hpq
• Polynomial.comp_eq_aeval 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] {p q : Polynomial R} : p.comp q = (Polynomial.aeval q) p
• Polynomial.algEquivOfCompEqX_eq_iff 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] (p q p' q' : Polynomial R) (hpq : p.comp q = Polynomial.X) (hqp : q.comp p = Polynomial.X) (hpq' : p'.comp q' = Polynomial.X) (hqp' : q'.comp p' = Polynomial.X) : p.algEquivOfCompEqX q hpq hqp = p'.algEquivOfCompEqX q' hpq' hqp' ↔ p = p'
• Polynomial.dvd_comp_neg_X_iff 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommRing R] (p q : Polynomial R) : p ∣ q.comp (-Polynomial.X) ↔ p.comp (-Polynomial.X) ∣ q
• Polynomial.aeval_comp 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] {p q : Polynomial R} {A : Type u_3} [Semiring A] [Algebra R A] (x : A) : (Polynomial.aeval x) (p.comp q) = (Polynomial.aeval ((Polynomial.aeval x) q)) p
• Polynomial.algEquivOfCompEqX_apply 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] (p q : Polynomial R) (hpq : p.comp q = Polynomial.X) (hqp : q.comp p = Polynomial.X) (a : Polynomial R) : (p.algEquivOfCompEqX q hpq hqp) a = (Polynomial.aeval p) a
• Polynomial.dvd_comp_X_add_C_iff 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommRing R] (p q : Polynomial R) (a : R) : p ∣ q.comp (Polynomial.X + Polynomial.C a) ↔ p.comp (Polynomial.X - Polynomial.C a) ∣ q
• Polynomial.dvd_comp_X_sub_C_iff 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommRing R] (p q : Polynomial R) (a : R) : p ∣ q.comp (Polynomial.X - Polynomial.C a) ↔ p.comp (Polynomial.X + Polynomial.C a) ∣ q
• Polynomial.X_sub_C_pow_dvd_iff 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} : (Polynomial.X - Polynomial.C t) ^ n ∣ p ↔ Polynomial.X ^ n ∣ p.comp (Polynomial.X + Polynomial.C t)
• Polynomial.dvd_comp_C_mul_X_add_C_iff 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommRing R] (p q : Polynomial R) (a b : R) [Invertible a] : p ∣ q.comp (Polynomial.C a * Polynomial.X + Polynomial.C b) ↔ p.comp (Polynomial.C ⅟a * (Polynomial.X - Polynomial.C b)) ∣ q
• Polynomial.natDegree_comp_le 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Semiring R] {p q : Polynomial R} : (p.comp q).natDegree ≤ p.natDegree * q.natDegree
• Polynomial.degree_comp_neg_X 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Ring R] {p : Polynomial R} : (p.comp (-Polynomial.X)).degree = p.degree
• Polynomial.natDegree_comp 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Semiring R] {p q : Polynomial R} [NoZeroDivisors R] : (p.comp q).natDegree = p.natDegree * q.natDegree
• Polynomial.natDegree_iterate_comp 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Semiring R] {p q : Polynomial R} [NoZeroDivisors R] (k : ℕ) : (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
• Polynomial.comp_neg_X_eq_zero_iff 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Ring R] {p : Polynomial R} : p.comp (-Polynomial.X) = 0 ↔ p = 0
• Polynomial.leadingCoeff_comp 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Semiring R] {p q : Polynomial R} [NoZeroDivisors R] (hq : q.natDegree ≠ 0) : (p.comp q).leadingCoeff = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
• Polynomial.natDegree_comp_eq_of_mul_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0) : (p.comp q).natDegree = p.natDegree * q.natDegree
• Polynomial.comp_neg_X_leadingCoeff_eq 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Ring R] (p : Polynomial R) : (p.comp (-Polynomial.X)).leadingCoeff = (-1) ^ p.natDegree * p.leadingCoeff
• Polynomial.degree_comp 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} (hq : 0 < q.degree) : (p.comp q).degree = p.degree * q.degree
• Polynomial.comp_eq_zero_iff 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} : p.comp q = 0 ↔ p = 0 ∨ Polynomial.eval (q.coeff 0) p = 0 ∧ q = Polynomial.C (q.coeff 0)
• Polynomial.Monic.comp 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q.Monic) (h : q.natDegree ≠ 0) : (p.comp q).Monic
• Polynomial.Monic.comp_X_add_C 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (r : R) : (p.comp (Polynomial.X + Polynomial.C r)).Monic
• Polynomial.Monic.comp_X_sub_C 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Ring R] {p : Polynomial R} (hp : p.Monic) (r : R) : (p.comp (Polynomial.X - Polynomial.C r)).Monic
• Polynomial.geom_sum_X_comp_X_add_one_eq_sum 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : (∑ i ∈ Finset.range n, Polynomial.X ^ i).comp (Polynomial.X + 1) = ∑ i ∈ Finset.range n, ↑(n.choose (i + 1)) * Polynomial.X ^ i
• Polynomial.derivative_comp 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] (p q : Polynomial R) : Polynomial.derivative (p.comp q) = Polynomial.derivative q * (Polynomial.derivative p).comp q
• Polynomial.derivative_comp_one_sub_X 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommRing R] (p : Polynomial R) : Polynomial.derivative (p.comp (1 - Polynomial.X)) = -(Polynomial.derivative p).comp (1 - Polynomial.X)
• Polynomial.iterate_derivative_comp_one_sub_X 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommRing R] (p : Polynomial R) (k : ℕ) : (⇑Polynomial.derivative)^[k] (p.comp (1 - Polynomial.X)) = (-1) ^ k * ((⇑Polynomial.derivative)^[k] p).comp (1 - Polynomial.X)
• Polynomial.eval_divByMonic_eq_trailingCoeff_comp 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} : Polynomial.eval t (p /ₘ (Polynomial.X - Polynomial.C t) ^ Polynomial.rootMultiplicity t p) = (p.comp (Polynomial.X + Polynomial.C t)).trailingCoeff
• Polynomial.rootMultiplicity_eq_natTrailingDegree 📋 Mathlib.Algebra.Polynomial.RingDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} : Polynomial.rootMultiplicity t p = (p.comp (Polynomial.X + Polynomial.C t)).natTrailingDegree
• Polynomial.rootMultiplicity_eq_rootMultiplicity 📋 Mathlib.Algebra.Polynomial.RingDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} : Polynomial.rootMultiplicity t p = Polynomial.rootMultiplicity 0 (p.comp (Polynomial.X + Polynomial.C t))
• Polynomial.Monic.neg_one_pow_natDegree_mul_comp_neg_X 📋 Mathlib.Algebra.Polynomial.RingDivision
  {R : Type u} [CommRing R] {p : Polynomial R} (hp : p.Monic) : ((-1) ^ p.natDegree * p.comp (-Polynomial.X)).Monic
• Polynomial.rootMultiplicity_comp_C_mul_X_add_C 📋 Mathlib.Algebra.Polynomial.RingDivision
  {R : Type u} [CommRing R] (p : Polynomial R) (a b c : R) (ha : IsUnit a) : Polynomial.rootMultiplicity c (p.comp (Polynomial.C a * Polynomial.X + Polynomial.C b)) = Polynomial.rootMultiplicity (a * c + b) p
• Polynomial.expand_eq_comp_X_pow 📋 Mathlib.Algebra.Polynomial.Expand
  {R : Type u} [CommSemiring R] (p : ℕ) {f : Polynomial R} : (Polynomial.expand R p) f = f.comp (Polynomial.X ^ p)
• Polynomial.smul_comp 📋 Mathlib.Algebra.Polynomial.Eval.SMul
  {R : Type u} {S : Type v} [Semiring R] [SMulZeroClass S R] [IsScalarTower S R R] (s : S) (p q : Polynomial R) : (s • p).comp q = s • p.comp q
• Polynomial.roots_comp_neg_X 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) : (p.comp (-Polynomial.X)).roots = Multiset.map (fun x => -x) p.roots
• Polynomial.map_roots_comp_C_mul_X_add_C 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) (a b : R) (ha : IsUnit a) : Multiset.map (fun x => a * x + b) (p.comp (Polynomial.C a * Polynomial.X + Polynomial.C b)).roots = p.roots
• Polynomial.roots_comp_C_mul_X_add_C 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) (a b : R) (ha : IsUnit a) : (p.comp (Polynomial.C a * Polynomial.X + Polynomial.C b)).roots = Multiset.map (fun x => Ring.inverse a * (x - b)) p.roots
• Matrix.charpoly_sub_scalar 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
  {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) (μ : R) : (M - (Matrix.scalar n) μ).charpoly = M.charpoly.comp (Polynomial.X + Polynomial.C μ)
• Polynomial.taylor_apply 📋 Mathlib.Algebra.Polynomial.Taylor
  {R : Type u_1} [Semiring R] (r : R) (f : Polynomial R) : (Polynomial.taylor r) f = f.comp (Polynomial.X + Polynomial.C r)
• Polynomial.Splits.comp_neg_X 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Ring R] {f : Polynomial R} (hf : f.Splits) : (f.comp (-Polynomial.X)).Splits
• Polynomial.Splits.comp_of_natDegree_le_one_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.natDegree ≤ 1) (h : g.Monic) : (f.comp g).Splits
• Polynomial.Splits.comp_of_degree_le_one_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.degree ≤ 1) (h : g.Monic) : (f.comp g).Splits
• Polynomial.splits_iff_comp_splits_of_natDegree_eq_one 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f g : Polynomial R} (hg : g.natDegree = 1) : f.Splits ↔ (f.comp g).Splits
• Polynomial.Splits.comp_of_natDegree_le_one 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f g : Polynomial R} (hf : f.Splits) (hg : g.natDegree ≤ 1) : (f.comp g).Splits
• Polynomial.Splits.comp_of_natDegree_le_one_of_invertible 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.natDegree ≤ 1) (h : Invertible g.leadingCoeff) : (f.comp g).Splits
• Polynomial.splits_iff_comp_splits_of_degree_eq_one 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f g : Polynomial R} (hg : g.degree = 1) : f.Splits ↔ (f.comp g).Splits
• Polynomial.Splits.comp_of_degree_le_one 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f g : Polynomial R} (hf : f.Splits) (hg : g.degree ≤ 1) : (f.comp g).Splits
• Polynomial.Splits.comp_of_degree_le_one_of_invertible 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.degree ≤ 1) (h : Invertible g.leadingCoeff) : (f.comp g).Splits
• Polynomial.Splits.comp_X_add_C 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f : Polynomial R} (hf : f.Splits) (a : R) : (f.comp (Polynomial.X + Polynomial.C a)).Splits
• Polynomial.Splits.comp_X_sub_C 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Splits) (a : R) : (f.comp (Polynomial.X - Polynomial.C a)).Splits
• PolynomialModule.comp_smul 📋 Mathlib.Algebra.Polynomial.Module.Basic
  {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (p p' : Polynomial R) (q : PolynomialModule R M) : (PolynomialModule.comp p) (p' • q) = p'.comp p • (PolynomialModule.comp p) q
• minpoly.neg 📋 Mathlib.FieldTheory.Minpoly.Field
  {A : Type u_1} [Field A] {B : Type u_3} [Ring B] [Algebra A B] (x : B) : minpoly A (-x) = (-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-Polynomial.X)
• minpoly.add_algebraMap 📋 Mathlib.FieldTheory.Minpoly.Field
  {A : Type u_1} [Field A] {B : Type u_3} [CommRing B] [Algebra A B] (x : B) (a : A) : minpoly A (x + (algebraMap A B) a) = (minpoly A x).comp (Polynomial.X - Polynomial.C a)
• minpoly.sub_algebraMap 📋 Mathlib.FieldTheory.Minpoly.Field
  {A : Type u_1} [Field A] {B : Type u_3} [CommRing B] [Algebra A B] (x : B) (a : A) : minpoly A (x - (algebraMap A B) a) = (minpoly A x).comp (Polynomial.X + Polynomial.C a)
• Polynomial.irreducible_comp 📋 Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
  {K : Type u} [Field K] {f g : Polynomial K} (hfm : f.Monic) (hgm : g.Monic) (hf : Irreducible f) (hg : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - Polynomial.C (IntermediateField.AdjoinSimple.gen K x))) : Irreducible (f.comp g)
• ascPochhammer_eval_comp 📋 Mathlib.RingTheory.Polynomial.Pochhammer
  {S : Type u} [Semiring S] {R : Type u_1} [CommSemiring R] (n : ℕ) (p : Polynomial R) [Algebra R S] (x : S) : Polynomial.eval x ((ascPochhammer S n).comp (Polynomial.map (algebraMap R S) p)) = Polynomial.eval (Polynomial.eval₂ (algebraMap R S) x p) (ascPochhammer S n)
• descPochhammer_eq_ascPochhammer 📋 Mathlib.RingTheory.Polynomial.Pochhammer
  (n : ℕ) : descPochhammer ℤ n = (ascPochhammer ℤ n).comp (Polynomial.X - ↑n + 1)
• ascPochhammer_mul 📋 Mathlib.RingTheory.Polynomial.Pochhammer
  (S : Type u) [Semiring S] (n m : ℕ) : ascPochhammer S n * (ascPochhammer S m).comp (Polynomial.X + ↑n) = ascPochhammer S (n + m)
• ascPochhammer_succ_left 📋 Mathlib.RingTheory.Polynomial.Pochhammer
  (S : Type u) [Semiring S] (n : ℕ) : ascPochhammer S (n + 1) = Polynomial.X * (ascPochhammer S n).comp (Polynomial.X + 1)
• descPochhammer_mul 📋 Mathlib.RingTheory.Polynomial.Pochhammer
  (R : Type u) [Ring R] (n m : ℕ) : descPochhammer R n * (descPochhammer R m).comp (Polynomial.X - ↑n) = descPochhammer R (n + m)
• descPochhammer_succ_left 📋 Mathlib.RingTheory.Polynomial.Pochhammer
  (R : Type u) [Ring R] (n : ℕ) : descPochhammer R (n + 1) = Polynomial.X * (descPochhammer R n).comp (Polynomial.X - 1)
• ascPochhammer_succ_comp_X_add_one 📋 Mathlib.RingTheory.Polynomial.Pochhammer
  (S : Type u) [Semiring S] (n : ℕ) : (ascPochhammer S (n + 1)).comp (Polynomial.X + 1) = ascPochhammer S (n + 1) + (n + 1) • (ascPochhammer S n).comp (Polynomial.X + 1)
• descPochhammer_succ_comp_X_sub_one 📋 Mathlib.RingTheory.Polynomial.Pochhammer
  (R : Type u) [Ring R] (n : ℕ) : (descPochhammer R (n + 1)).comp (Polynomial.X - 1) = descPochhammer R (n + 1) - (↑n + 1) • (descPochhammer R n).comp (Polynomial.X - 1)
• Polynomial.Chebyshev.C_mul 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  (R : Type u_1) [CommRing R] (m n : ℤ) : Polynomial.Chebyshev.C R (m * n) = (Polynomial.Chebyshev.C R m).comp (Polynomial.Chebyshev.C R n)
• Polynomial.Chebyshev.T_mul 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  (R : Type u_1) [CommRing R] (m n : ℤ) : Polynomial.Chebyshev.T R (m * n) = (Polynomial.Chebyshev.T R m).comp (Polynomial.Chebyshev.T R n)
• Polynomial.Chebyshev.S_comp_two_mul_X 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  (R : Type u_1) [CommRing R] (n : ℤ) : (Polynomial.Chebyshev.S R n).comp (2 * Polynomial.X) = Polynomial.Chebyshev.U R n
• Polynomial.Chebyshev.C_comp_two_mul_X 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  (R : Type u_1) [CommRing R] (n : ℤ) : (Polynomial.Chebyshev.C R n).comp (2 * Polynomial.X) = 2 * Polynomial.Chebyshev.T R n
• Polynomial.Chebyshev.S_eq_U_comp_half_mul_X 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  (R : Type u_1) [CommRing R] [Invertible 2] (n : ℤ) : Polynomial.Chebyshev.S R n = (Polynomial.Chebyshev.U R n).comp (Polynomial.C ⅟2 * Polynomial.X)
• Polynomial.Chebyshev.C_eq_two_mul_T_comp_half_mul_X 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  (R : Type u_1) [CommRing R] [Invertible 2] (n : ℤ) : Polynomial.Chebyshev.C R n = 2 * (Polynomial.Chebyshev.T R n).comp (Polynomial.C ⅟2 * Polynomial.X)
• Polynomial.Chebyshev.T_eq_half_mul_C_comp_two_mul_X 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  (R : Type u_1) [CommRing R] [Invertible 2] (n : ℤ) : Polynomial.Chebyshev.T R n = Polynomial.C ⅟2 * (Polynomial.Chebyshev.C R n).comp (2 * Polynomial.X)
• LinearMap.charpoly_sub_smul 📋 Mathlib.LinearAlgebra.Charpoly.Basic
  {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : Module.End R M) (μ : R) : LinearMap.charpoly (f - μ • 1) = (LinearMap.charpoly f).comp (Polynomial.X + Polynomial.C μ)
• Polynomial.IsMonicOfDegree.comp 📋 Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
  {R : Type u_1} [Semiring R] {p q : Polynomial R} {m n : ℕ} (hn : n ≠ 0) (hp : p.IsMonicOfDegree m) (hq : q.IsMonicOfDegree n) : (p.comp q).IsMonicOfDegree (m * n)
• Polynomial.smeval_comp 📋 Mathlib.Algebra.Polynomial.Smeval
  (R : Type u_1) [Semiring R] (p q : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ℕ] (x : S) [NatPowAssoc S] [IsScalarTower R S S] [SMulCommClass R S S] : (p.comp q).smeval x = p.smeval (q.smeval x)
• Polynomial.Gal.restrictComp 📋 Mathlib.FieldTheory.PolynomialGaloisGroup
  {F : Type u_1} [Field F] (p q : Polynomial F) (hq : q.natDegree ≠ 0) : (p.comp q).Gal →* p.Gal
• Polynomial.Gal.splits_in_splittingField_of_comp 📋 Mathlib.FieldTheory.PolynomialGaloisGroup
  {F : Type u_1} [Field F] (p q : Polynomial F) (hq : q.natDegree ≠ 0) : (Polynomial.map (algebraMap F (p.comp q).SplittingField) p).Splits
• Polynomial.Gal.restrictComp_surjective 📋 Mathlib.FieldTheory.PolynomialGaloisGroup
  {F : Type u_1} [Field F] (p q : Polynomial F) (hq : q.natDegree ≠ 0) : Function.Surjective ⇑(Polynomial.Gal.restrictComp p q hq)
• bernsteinPolynomial.flip 📋 Mathlib.RingTheory.Polynomial.Bernstein
  (R : Type u_1) [CommRing R] (n ν : ℕ) (h : ν ≤ n) : (bernsteinPolynomial R n ν).comp (1 - Polynomial.X) = bernsteinPolynomial R n (n - ν)
• bernsteinPolynomial.flip' 📋 Mathlib.RingTheory.Polynomial.Bernstein
  (R : Type u_1) [CommRing R] (n ν : ℕ) (h : ν ≤ n) : bernsteinPolynomial R n ν = (bernsteinPolynomial R n (n - ν)).comp (1 - Polynomial.X)
• IsPrimitiveRoot.minpoly_sub_one_eq_cyclotomic_comp 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] {A : Type w} {K : Type u} [CommRing A] [Field K] [Algebra K A] [IsDomain A] {ζ : A} [IsCyclotomicExtension {n} K A] (hζ : IsPrimitiveRoot ζ n) (h : Irreducible (Polynomial.cyclotomic n K)) : minpoly K (ζ - 1) = (Polynomial.cyclotomic n K).comp (Polynomial.X + 1)
• Polynomial.bernoulli_comp_one_sub_X 📋 Mathlib.NumberTheory.BernoulliPolynomials
  (n : ℕ) : (Polynomial.bernoulli n).comp (1 - Polynomial.X) = (-1) ^ n * Polynomial.bernoulli n
• Polynomial.bernoulli_comp_one_add_X 📋 Mathlib.NumberTheory.BernoulliPolynomials
  (n : ℕ) : (Polynomial.bernoulli n).comp (1 + Polynomial.X) = Polynomial.bernoulli n + n • Polynomial.X ^ (n - 1)
• Polynomial.bernoulli_comp_neg_X 📋 Mathlib.NumberTheory.BernoulliPolynomials
  (n : ℕ) : (Polynomial.bernoulli n).comp (-Polynomial.X) = (-1) ^ n • (Polynomial.bernoulli n + n • Polynomial.X ^ (n - 1))
• cyclotomic_comp_X_add_one_isEisensteinAt 📋 Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
  (p : ℕ) [hp : Fact (Nat.Prime p)] : ((Polynomial.cyclotomic p ℤ).comp (Polynomial.X + 1)).IsEisensteinAt (ℤ ∙ ↑p)
• cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt 📋 Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
  (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : ((Polynomial.cyclotomic (p ^ (n + 1)) ℤ).comp (Polynomial.X + 1)).IsEisensteinAt (ℤ ∙ ↑p)
• Polynomial.dickson_one_one_mul 📋 Mathlib.RingTheory.Polynomial.Dickson
  (R : Type u_1) [CommRing R] (m n : ℕ) : Polynomial.dickson 1 1 (m * n) = (Polynomial.dickson 1 1 m).comp (Polynomial.dickson 1 1 n)
• Polynomial.dickson_one_one_comp_comm 📋 Mathlib.RingTheory.Polynomial.Dickson
  (R : Type u_1) [CommRing R] (m n : ℕ) : (Polynomial.dickson 1 1 m).comp (Polynomial.dickson 1 1 n) = (Polynomial.dickson 1 1 n).comp (Polynomial.dickson 1 1 m)
• Polynomial.chebyshev_U_eq_dickson_two_one 📋 Mathlib.RingTheory.Polynomial.Dickson
  (R : Type u_1) [CommRing R] (n : ℕ) : Polynomial.Chebyshev.U R ↑n = (Polynomial.dickson 2 1 n).comp (2 * Polynomial.X)
• Polynomial.dickson_two_one_eq_chebyshev_U 📋 Mathlib.RingTheory.Polynomial.Dickson
  (R : Type u_1) [CommRing R] [Invertible 2] (n : ℕ) : Polynomial.dickson 2 1 n = (Polynomial.Chebyshev.U R ↑n).comp (Polynomial.C ⅟2 * Polynomial.X)
• Polynomial.chebyshev_T_eq_dickson_one_one 📋 Mathlib.RingTheory.Polynomial.Dickson
  (R : Type u_1) [CommRing R] [Invertible 2] (n : ℕ) : Polynomial.Chebyshev.T R ↑n = Polynomial.C ⅟2 * (Polynomial.dickson 1 1 n).comp (2 * Polynomial.X)
• Polynomial.dickson_one_one_eq_chebyshev_T 📋 Mathlib.RingTheory.Polynomial.Dickson
  (R : Type u_1) [CommRing R] [Invertible 2] (n : ℕ) : Polynomial.dickson 1 1 n = 2 * (Polynomial.Chebyshev.T R ↑n).comp (Polynomial.C ⅟2 * Polynomial.X)
• Polynomial.neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq 📋 Mathlib.RingTheory.Polynomial.ShiftedLegendre
  (n : ℕ) : (-1) ^ n * (Polynomial.shiftedLegendre n).comp (1 - Polynomial.X) = Polynomial.shiftedLegendre n

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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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

4. 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.

5. 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