Loogle!

Result

Found 15 declarations mentioning Cubic.map.

• Cubic.map 📋 Mathlib.Algebra.CubicDiscriminant
  {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (φ : R →+* S) (P : Cubic R) : Cubic S
• Cubic.map_toPoly 📋 Mathlib.Algebra.CubicDiscriminant
  {R : Type u_1} {S : Type u_2} {P : Cubic R} [Semiring R] [Semiring S] {φ : R →+* S} : (Cubic.map φ P).toPoly = Polynomial.map φ P.toPoly
• Cubic.map_roots 📋 Mathlib.Algebra.CubicDiscriminant
  {R : Type u_1} {S : Type u_2} {P : Cubic R} [CommRing R] [CommRing S] {φ : R →+* S} [IsDomain S] : (Cubic.map φ P).roots = (Polynomial.map φ P.toPoly).roots
• Cubic.splits_iff_card_roots 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} (ha : P.a ≠ 0) : Polynomial.Splits φ P.toPoly ↔ (Cubic.map φ P).roots.card = 3
• Cubic.map.eq_1 📋 Mathlib.Algebra.CubicDiscriminant
  {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (φ : R →+* S) (P : Cubic R) : Cubic.map φ P = { a := φ P.a, b := φ P.b, c := φ P.c, d := φ P.d }
• Cubic.splits_iff_roots_eq_three 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} (ha : P.a ≠ 0) : Polynomial.Splits φ P.toPoly ↔ ∃ x y z, (Cubic.map φ P).roots = {x, y, z}
• Cubic.disc_ne_zero_iff_roots_ne 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x y z : K} (ha : P.a ≠ 0) (h3 : (Cubic.map φ P).roots = {x, y, z}) : P.disc ≠ 0 ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z
• Cubic.disc_ne_zero_iff_roots_nodup 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x y z : K} (ha : P.a ≠ 0) (h3 : (Cubic.map φ P).roots = {x, y, z}) : P.disc ≠ 0 ↔ (Cubic.map φ P).roots.Nodup
• Cubic.card_roots_of_disc_ne_zero 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x y z : K} [DecidableEq K] (ha : P.a ≠ 0) (h3 : (Cubic.map φ P).roots = {x, y, z}) (hd : P.disc ≠ 0) : (Cubic.map φ P).roots.toFinset.card = 3
• Cubic.b_eq_three_roots 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x y z : K} (ha : P.a ≠ 0) (h3 : (Cubic.map φ P).roots = {x, y, z}) : φ P.b = φ P.a * -(x + y + z)
• Cubic.d_eq_three_roots 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x y z : K} (ha : P.a ≠ 0) (h3 : (Cubic.map φ P).roots = {x, y, z}) : φ P.d = φ P.a * -(x * y * z)
• Cubic.c_eq_three_roots 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x y z : K} (ha : P.a ≠ 0) (h3 : (Cubic.map φ P).roots = {x, y, z}) : φ P.c = φ P.a * (x * y + x * z + y * z)
• Cubic.disc_eq_prod_three_roots 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x y z : K} (ha : P.a ≠ 0) (h3 : (Cubic.map φ P).roots = {x, y, z}) : φ P.disc = (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
• Cubic.eq_sum_three_roots 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x y z : K} (ha : P.a ≠ 0) (h3 : (Cubic.map φ P).roots = {x, y, z}) : Cubic.map φ P = { a := φ P.a, b := φ P.a * -(x + y + z), c := φ P.a * (x * y + x * z + y * z), d := φ P.a * -(x * y * z) }
• Cubic.eq_prod_three_roots 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x y z : K} (ha : P.a ≠ 0) (h3 : (Cubic.map φ P).roots = {x, y, z}) : (Cubic.map φ P).toPoly = Polynomial.C (φ P.a) * (Polynomial.X - Polynomial.C x) * (Polynomial.X - Polynomial.C y) * (Polynomial.X - Polynomial.C 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