Loogle!

Result

Found 10 declarations mentioning PowerBasis.map.

• PowerBasis.map 📋 Mathlib.RingTheory.PowerBasis
  {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_7} [CommRing S'] [Algebra R S'] (pb : PowerBasis R S) (e : S ≃ₐ[R] S') : PowerBasis R S'
• PowerBasis.map_dim 📋 Mathlib.RingTheory.PowerBasis
  {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_7} [CommRing S'] [Algebra R S'] (pb : PowerBasis R S) (e : S ≃ₐ[R] S') : (pb.map e).dim = pb.dim
• PowerBasis.minpolyGen_map 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] {S' : Type u_7} [CommRing S'] [Algebra A S] [Algebra A S'] (pb : PowerBasis A S) (e : S ≃ₐ[A] S') : (pb.map e).minpolyGen = pb.minpolyGen
• PowerBasis.map_gen 📋 Mathlib.RingTheory.PowerBasis
  {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_7} [CommRing S'] [Algebra R S'] (pb : PowerBasis R S) (e : S ≃ₐ[R] S') : (pb.map e).gen = e pb.gen
• PowerBasis.equivOfMinpoly_map 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] {S' : Type u_7} [CommRing S'] [Algebra A S] [Algebra A S'] (pb : PowerBasis A S) (e : S ≃ₐ[A] S') (h : minpoly A pb.gen = minpoly A (pb.map e).gen) : pb.equivOfMinpoly (pb.map e) h = e
• PowerBasis.map_basis 📋 Mathlib.RingTheory.PowerBasis
  {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_7} [CommRing S'] [Algebra R S'] (pb : PowerBasis R S) (e : S ≃ₐ[R] S') : (pb.map e).basis = pb.basis.map e.toLinearEquiv
• PowerBasis.equivOfRoot_map 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] {S' : Type u_7} [CommRing S'] [Algebra A S] [Algebra A S'] (pb : PowerBasis A S) (e : S ≃ₐ[A] S') (h₁ : (Polynomial.aeval pb.gen) (minpoly A (pb.map e).gen) = 0) (h₂ : (Polynomial.aeval (pb.map e).gen) (minpoly A pb.gen) = 0) : pb.equivOfRoot (pb.map e) h₁ h₂ = e
• Algebra.adjoin.powerBasis'.eq_1 📋 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) : Algebra.adjoin.powerBasis' hx = (AdjoinRoot.powerBasis' ⋯).map (minpoly.equivAdjoin hx)
• PowerBasis.ofGenMemAdjoin'.eq_1 📋 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} (B : PowerBasis R S) (hint : IsIntegral R x) (hx : B.gen ∈ Algebra.adjoin R {x}) : B.ofGenMemAdjoin' hint hx = (Algebra.adjoin.powerBasis' hint).map (((Algebra.adjoin R {x}).equivOfEq ⊤ ⋯).trans Subalgebra.topEquiv)
• IsPrimitiveRoot.integralPowerBasis.eq_1 📋 Mathlib.NumberTheory.Cyclotomic.Rat
  {p : ℕ+} {k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime ↑p)] [CharZero K] [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : hζ.integralPowerBasis = (Algebra.adjoin.powerBasis' ⋯).map hζ.adjoinEquivRingOfIntegers

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