Loogle!

Result

Found 24 declarations mentioning IsAdjoinRoot.map.

• IsAdjoinRoot.map 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {f : Polynomial R} (self : IsAdjoinRoot S f) : Polynomial R →+* S
• IsAdjoinRoot.algebraMap_eq 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {f : Polynomial R} (self : IsAdjoinRoot S f) : algebraMap R S = self.map.comp Polynomial.C
• IsAdjoinRoot.map_surjective 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {f : Polynomial R} (self : IsAdjoinRoot S f) : Function.Surjective ⇑self.map
• AdjoinRoot.isAdjoinRoot_map_eq_mk 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} [CommRing R] (f : Polynomial R) : (AdjoinRoot.isAdjoinRoot f).map = AdjoinRoot.mk f
• IsAdjoinRoot.map_repr 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) (x : S) : h.map (h.repr x) = x
• IsAdjoinRoot.map_X 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) : h.map Polynomial.X = h.root
• IsAdjoinRoot.root.eq_1 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) : h.root = h.map Polynomial.X
• IsAdjoinRoot.map_self 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) : h.map f = 0
• AdjoinRoot.isAdjoinRootMonic_map_eq_mk 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} [CommRing R] (f : Polynomial R) (hf : f.Monic) : (AdjoinRoot.isAdjoinRootMonic f hf).map = AdjoinRoot.mk f
• IsAdjoinRoot.ker_map 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {f : Polynomial R} (self : IsAdjoinRoot S f) : RingHom.ker self.map = Ideal.span {f}
• IsAdjoinRootMonic.modByMonic_repr_map 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (g : Polynomial R) : h.repr (h.map g) %ₘ f = g %ₘ f
• IsAdjoinRoot.map_eq_zero_iff 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {p : Polynomial R} : h.map p = 0 ↔ f ∣ p
• IsAdjoinRoot.eval₂_repr_eq_eval₂_of_map_eq 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] {T : Type u_1} [CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0) (h : IsAdjoinRoot S f) (z : S) (w : Polynomial R) (hzw : h.map w = z) : Polynomial.eval₂ i x (h.repr z) = Polynomial.eval₂ i x w
• IsAdjoinRoot.ext_map 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h h' : IsAdjoinRoot S f) (eq : ∀ (x : Polynomial R), h.map x = h'.map x) : h = h'
• IsAdjoinRoot.aeval_eq 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) (p : Polynomial R) : (Polynomial.aeval h.root) p = h.map p
• IsAdjoinRootMonic.map_modByMonic 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (g : Polynomial R) : h.map (g %ₘ f) = h.map g
• IsAdjoinRoot.algebraMap_apply 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) (x : R) : (algebraMap R S) x = h.map (Polynomial.C x)
• IsAdjoinRoot.lift_map 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] {T : Type u_1} [CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0) (h : IsAdjoinRoot S f) (z : Polynomial R) : (IsAdjoinRoot.lift i x h hx) (h.map z) = Polynomial.eval₂ i x z
• IsAdjoinRoot.aequiv_map 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} {T : Type u_1} [CommRing T] [Algebra R T] (h : IsAdjoinRoot S f) (h' : IsAdjoinRoot T f) (z : Polynomial R) : (h.aequiv h') (h.map z) = h'.map z
• IsAdjoinRoot.ofEquiv_map_apply 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} {T : Type u_1} [CommRing T] [Algebra R T] (h : IsAdjoinRoot S f) (e : S ≃ₐ[R] T) (a✝ : Polynomial R) : (h.ofEquiv e).map a✝ = e (h.map a✝)
• IsAdjoinRoot.mem_ker_map 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {p : Polynomial R} : p ∈ RingHom.ker h.map ↔ f ∣ p
• IsAdjoinRootMonic.map_modByMonicHom 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (x : S) : h.map (h.modByMonicHom x) = x
• IsAdjoinRootMonic.modByMonicHom_map 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (g : Polynomial R) : h.modByMonicHom (h.map g) = g %ₘ f
• IsAdjoinRoot.liftHom_map 📋 Mathlib.RingTheory.IsAdjoinRoot
  {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] {T : Type u_1} [CommRing T] {x : T} [Algebra R T] (hx' : (Polynomial.aeval x) f = 0) (h : IsAdjoinRoot S f) (z : Polynomial R) : (IsAdjoinRoot.liftHom x hx' h) (h.map z) = (Polynomial.aeval x) z

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

This is Loogle revision 19971e9 serving mathlib revision bce1d65