Loogle!

Result

Found 40 definitions mentioning Algebra.adjoin and Polynomial.

• Algebra.adjoin_singleton_eq_range_aeval 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) : Algebra.adjoin R {x} = (Polynomial.aeval x).range
• Polynomial.aeval_mem_adjoin_singleton 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {p : Polynomial R} (x : A) : (Polynomial.aeval x) p ∈ Algebra.adjoin R {x}
• Polynomial.adjoin_X 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] : Algebra.adjoin R {Polynomial.X} = ⊤
• Algebra.mem_ideal_map_adjoin 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] (x : S) (I : Ideal R) {y : ↥(Algebra.adjoin R {x})} : y ∈ Ideal.map (algebraMap R ↥(Algebra.adjoin R {x})) I ↔ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (Polynomial.aeval x) p = ↑y
• Submodule.span_range_natDegree_eq_adjoin 📋 Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
  {R : Type u_5} {A : Type u_6} [CommRing R] [Semiring A] [Algebra R A] {x : A} {f : Polynomial R} (hf : f.Monic) (hfx : (Polynomial.aeval x) f = 0) : Submodule.span R ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree)) = Subalgebra.toSubmodule (Algebra.adjoin R {x})
• adjoin_monomial_eq_reesAlgebra 📋 Mathlib.RingTheory.ReesAlgebra
  {R : Type u} [CommRing R] (I : Ideal R) : Algebra.adjoin R ↑(Submodule.map (Polynomial.monomial 1) I) = reesAlgebra I
• monomial_mem_adjoin_monomial 📋 Mathlib.RingTheory.ReesAlgebra
  {R : Type u} [CommRing R] {I : Ideal R} {n : ℕ} {r : R} (hr : r ∈ I ^ n) : (Polynomial.monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (Polynomial.monomial 1) I)
• Polynomial.adjoin_rootSet_eq_range 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} {K : Type v} {L : Type w} [CommRing R] [Field K] [Field L] [Algebra R K] [Algebra R L] {p : Polynomial R} (h : Polynomial.Splits (algebraMap R K) p) (f : K →ₐ[R] L) : Algebra.adjoin R (p.rootSet L) = f.range ↔ Algebra.adjoin R (p.rootSet K) = ⊤
• Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree 📋 Mathlib.RingTheory.Polynomial.Eisenstein.Basic
  {R : Type u} [CommRing R] {f : Polynomial R} {S : Type v} [CommRing S] [Algebra R S] {p : R} {x : S} (hx : (Polynomial.aeval x) f = 0) (hmo : f.Monic) (hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})) : ∃ y ∈ Algebra.adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
• Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree_le 📋 Mathlib.RingTheory.Polynomial.Eisenstein.Basic
  {R : Type u} [CommRing R] {f : Polynomial R} {S : Type v} [CommRing S] [Algebra R S] {p : R} {x : S} (hx : (Polynomial.aeval x) f = 0) (hmo : f.Monic) (hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})) (i : ℕ) : (Polynomial.map (algebraMap R S) f).natDegree ≤ i → ∃ y ∈ Algebra.adjoin R {x}, (algebraMap R S) p * y = x ^ i
• AdjoinRoot.adjoinRoot_eq_top 📋 Mathlib.RingTheory.AdjoinRoot
  {R : Type u} [CommRing R] {f : Polynomial R} : Algebra.adjoin R {AdjoinRoot.root f} = ⊤
• AdjoinRoot.Minpoly.toAdjoin.apply_X 📋 Mathlib.RingTheory.AdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {x : S} : (AdjoinRoot.Minpoly.toAdjoin R x) ((AdjoinRoot.mk (minpoly R x)) Polynomial.X) = ⟨x, ⋯⟩
• AdjoinRoot.Minpoly.toAdjoin_apply 📋 Mathlib.RingTheory.AdjoinRoot
  (R : Type u) {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (x : S) (a✝ : Polynomial R ⧸ Submodule.toAddSubgroup (Ideal.span {minpoly R x})) : (AdjoinRoot.Minpoly.toAdjoin R x) a✝ = (QuotientAddGroup.lift (Submodule.toAddSubgroup (Ideal.span {minpoly R x})) ↑(Polynomial.eval₂RingHom (algebraMap R ↥(Algebra.adjoin R {x})) ⟨x, ⋯⟩) ⋯) a✝
• AdjoinRoot.Minpoly.toAdjoin_apply' 📋 Mathlib.RingTheory.AdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {x : S} (a : AdjoinRoot (minpoly R x)) : (AdjoinRoot.Minpoly.toAdjoin R x) a = (AdjoinRoot.liftHom (minpoly R x) ⟨x, ⋯⟩ ⋯) a
• Algebra.adjoin.liftSingleton 📋 Mathlib.RingTheory.Adjoin.Field
  (F : Type u_1) [Field F] {S : Type u_2} {T : Type u_3} [CommRing S] [CommRing T] [Algebra F S] [Algebra F T] (x : S) (y : T) (h : (Polynomial.aeval y) (minpoly F x) = 0) : ↥(Algebra.adjoin F {x}) →ₐ[F] T
• Polynomial.IsSplittingField.adjoin_rootSet 📋 Mathlib.FieldTheory.SplittingField.IsSplittingField
  {K : Type v} (L : Type w) [Field K] [Field L] [Algebra K L] (f : Polynomial K) [Polynomial.IsSplittingField K L f] : Algebra.adjoin K (f.rootSet L) = ⊤
• Polynomial.IsSplittingField.adjoin_rootSet' 📋 Mathlib.FieldTheory.SplittingField.IsSplittingField
  {K : Type v} {L : Type w} {inst✝ : Field K} {inst✝¹ : Field L} {inst✝² : Algebra K L} {f : Polynomial K} [self : Polynomial.IsSplittingField K L f] : Algebra.adjoin K (f.rootSet L) = ⊤
• Polynomial.IsSplittingField.adjoin_rootSet_eq_range 📋 Mathlib.FieldTheory.SplittingField.IsSplittingField
  {F : Type u} {K : Type v} (L : Type w) [Field K] [Field L] [Field F] [Algebra K L] [Algebra K F] (f : Polynomial K) [Polynomial.IsSplittingField K L f] (i : L →ₐ[K] F) : Algebra.adjoin K (f.rootSet F) = i.range
• Polynomial.IsSplittingField.mk 📋 Mathlib.FieldTheory.SplittingField.IsSplittingField
  {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {f : Polynomial K} (splits' : Polynomial.Splits (algebraMap K L) f) (adjoin_rootSet' : Algebra.adjoin K (f.rootSet L) = ⊤) : Polynomial.IsSplittingField K L f
• Polynomial.SplittingFieldAux.adjoin_rootSet 📋 Mathlib.FieldTheory.SplittingField.Construction
  (n : ℕ) {K : Type u} [Field K] (f : Polynomial K) (_hfn : f.natDegree = n) : Algebra.adjoin K (f.rootSet (Polynomial.SplittingFieldAux n f)) = ⊤
• Polynomial.SplittingField.adjoin_rootSet 📋 Mathlib.FieldTheory.SplittingField.Construction
  {K : Type v} [Field K] (f : Polynomial K) : Algebra.adjoin K (f.rootSet f.SplittingField) = ⊤
• Module.End.exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow 📋 Mathlib.LinearAlgebra.JordanChevalley
  {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {f : Module.End K V} {P : Polynomial K} {k : ℕ} (sep : P.Separable) (nil : minpoly K f ∣ P ^ k) : ∃ n ∈ Algebra.adjoin K {f}, ∃ s ∈ Algebra.adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
• polynomialFunctions.eq_adjoin_X 📋 Mathlib.Topology.ContinuousMap.Polynomial
  {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] (s : Set R) : polynomialFunctions s = Algebra.adjoin R {(Polynomial.toContinuousMapOnAlgHom s) Polynomial.X}
• minpoly.equivAdjoin_symm_apply 📋 Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx : IsIntegral R x) (b : ↥(Algebra.adjoin R {x})) : (minpoly.equivAdjoin hx).symm b = Function.surjInv ⋯ b
• minpoly.equivAdjoin_apply 📋 Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx : IsIntegral R x) (a : AdjoinRoot (minpoly R x)) : (minpoly.equivAdjoin hx) a = (QuotientAddGroup.lift (Submodule.toAddSubgroup (Ideal.span {minpoly R x})) ↑(Polynomial.eval₂RingHom (algebraMap R ↥(Algebra.adjoin R {x})) ⟨x, ⋯⟩) ⋯) a
• sum_smul_minpolyDiv_eq_X_pow 📋 Mathlib.FieldTheory.Minpoly.MinpolyDiv
  {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] (E : Type u_1) [Field E] [Algebra K E] [IsAlgClosed E] [FiniteDimensional K L] [Algebra.IsSeparable K L] {x : L} (hxL : Algebra.adjoin K {x} = ⊤) {r : ℕ} (hr : r < Module.finrank K L) : ∑ σ : L →ₐ[K] E, Polynomial.map (↑σ) ((x ^ r / (Polynomial.aeval x) (Polynomial.derivative (minpoly K x))) • minpolyDiv K x) = Polynomial.X ^ r
• AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin 📋 Mathlib.RingTheory.AlgebraicIndependent
  {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) : MvPolynomial (Option ι) R ≃+* Polynomial ↥(Algebra.adjoin R (Set.range x))
• AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none 📋 Mathlib.RingTheory.AlgebraicIndependent
  {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) : hx.mvPolynomialOptionEquivPolynomialAdjoin (MvPolynomial.X none) = Polynomial.X
• AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some 📋 Mathlib.RingTheory.AlgebraicIndependent
  {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (i : ι) : hx.mvPolynomialOptionEquivPolynomialAdjoin (MvPolynomial.X (some i)) = Polynomial.C (hx.aevalEquiv (MvPolynomial.X i))
• AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C 📋 Mathlib.RingTheory.AlgebraicIndependent
  {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (r : R) : hx.mvPolynomialOptionEquivPolynomialAdjoin (MvPolynomial.C r) = Polynomial.C ((algebraMap R ↥(Algebra.adjoin R (Set.range x))) r)
• AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C' 📋 Mathlib.RingTheory.AlgebraicIndependent
  {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (r : R) : Polynomial.C (hx.aevalEquiv (MvPolynomial.C r)) = Polynomial.C ((algebraMap R ↥(Algebra.adjoin R (Set.range x))) r)
• AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply 📋 Mathlib.RingTheory.AlgebraicIndependent
  {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (y : MvPolynomial (Option ι) R) : hx.mvPolynomialOptionEquivPolynomialAdjoin y = Polynomial.map (↑hx.aevalEquiv) ((MvPolynomial.aeval fun o => o.elim Polynomial.X fun s => Polynomial.C (MvPolynomial.X s)) y)
• AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin 📋 Mathlib.RingTheory.AlgebraicIndependent
  {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (a : A) : (↑(Polynomial.aeval a)).comp hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom = ↑(MvPolynomial.aeval fun o => o.elim a x)
• Algebra.adjoin_root_eq_top_of_isSplittingField 📋 Mathlib.FieldTheory.KummerExtension
  {K : Type u} [Field K] {n : ℕ} (hζ : (primitiveRoots n K).Nonempty) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) {L : Type u_1} [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {α : L} (hα : α ^ n = (algebraMap K L) a) : Algebra.adjoin K {α} = ⊤
• mem_adjoin_of_dvd_coeff_of_dvd_aeval 📋 Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
  {A : Type u_1} {B : Type u_2} [CommSemiring A] [CommRing B] [Algebra A B] [NoZeroSMulDivisors A B] {Q : Polynomial A} {p : A} {x z : B} (hp : p ≠ 0) (hQ : ∀ i ∈ Finset.range (Q.natDegree + 1), p ∣ Q.coeff i) (hz : (Polynomial.aeval x) Q = p • z) : z ∈ Algebra.adjoin A {x}
• Algebra.adjoin.powerBasis'_minpoly_gen 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx' : IsIntegral R x) : minpoly R x = minpoly R (Algebra.adjoin.powerBasis' hx').gen
• KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk.eq_1 📋 Mathlib.NumberTheory.KummerDedekind
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [NoZeroSMulDivisors R S] (hI : I.IsMaximal) (hI' : I ≠ ⊥) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x) : KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx' = (normalizedFactorsEquivOfQuotEquiv ((quotAdjoinEquivQuotMap hx ⋯).symm.trans (((Algebra.adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (Ideal.quotEquivOfEq ⋯))) ⋯ ⋯).trans (normalizedFactorsEquivSpanNormalizedFactors ⋯).symm
• aeval_derivative_mem_differentIdeal 📋 Mathlib.RingTheory.DedekindDomain.Different
  (A : Type u_1) (K : Type u_2) (L : Type u) {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsIntegrallyClosed A] [IsDedekindDomain B] [NoZeroSMulDivisors A B] (x : B) (hx : Algebra.adjoin K {(algebraMap B L) x} = ⊤) : (Polynomial.aeval x) (Polynomial.derivative (minpoly A x)) ∈ differentIdeal A B
• conductor_mul_differentIdeal 📋 Mathlib.RingTheory.DedekindDomain.Different
  (A : Type u_1) (K : Type u_2) (L : Type u) {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsIntegrallyClosed A] [IsDedekindDomain B] [NoZeroSMulDivisors A B] (x : B) (hx : Algebra.adjoin K {(algebraMap B L) x} = ⊤) : conductor A x * differentIdeal A B = Ideal.span {(Polynomial.aeval x) (Polynomial.derivative (minpoly A x))}
• traceForm_dualSubmodule_adjoin 📋 Mathlib.RingTheory.DedekindDomain.Different
  (A : Type u_1) (K : Type u_2) {L : Type u} [CommRing A] [Field K] [Field L] [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegrallyClosed A] {x : L} (hx : Algebra.adjoin K {x} = ⊤) (hAx : IsIntegral A x) : (Algebra.traceForm K L).dualSubmodule (Subalgebra.toSubmodule (Algebra.adjoin A {x})) = ((Polynomial.aeval x) (Polynomial.derivative (minpoly K x)))⁻¹ • Subalgebra.toSubmodule (Algebra.adjoin A {x})

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. 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.

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, _ * _, _ ^ _, |- _ < _ → _
woould 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.

This is Loogle revision 4e1aab0 serving mathlib revision 2d53f5f