[Merged by Bors] - feat(*): localized R[X] notation for polynomial R

[pechersky]

I did not change polynomial (complex_term_here taking args) in many places because I thought it would be more confusing. Also, in some files that prove things about polynomials incidentally, I also did not include the notation and change the files.

---

[eric-wieser]

Is there anything that should have higher precedence? Should we be setting the precedence of the R too, perhaps by defining this as postfix?

[pechersky]

I copied the precedence of notation for non zero divisors. That's the only combo notation I've seen so far, and these two values allow for talking about non zero divisors of polynomial R without any parentheses.

If we come up another usage we can play around with the precedence. I also think this works properly with the multiplicative opposite right now.

[ocfnash]

Thank you so much for doing this; I am very much in favour of this.

Given the size of the diff, do you think it would be easy to use https://github.com/leanprover-community/leancrawler to show that this really is only changing notation?

A long time ago I did something similar to show that I didn't accidentally change anything while doing a large refactor and it was fairly easy.

[pechersky]

Given the size of the diff, do you think it would be easy to use https://github.com/leanprover-community/leancrawler to show that this really is only changing notation?

I tried running it an all.lean, but the output yaml was not compatible with pyyaml because of \Bbbk characters.

In lieu of that:
all changed lines:

❯ git diff 6787a8d926ff7fb3f287a4957e21bc93a321d8d4 pechersky/polynomial-notation -U0 --word-diff | grep -F "{+" -c
1919

adding the open_locale:

❯ git diff 6787a8d926ff7fb3f287a4957e21bc93a321d8d4 pechersky/polynomial-notation -U0 --word-diff | grep -F "{+" | grep open_locale -c
107

replacements:

❯ git diff 6787a8d926ff7fb3f287a4957e21bc93a321d8d4 pechersky/polynomial-notation -U0 --word-diff | grep -F "{+" | grep -o "\[-.*+\}" -c
1805

The 7 lines not covered by the previous examples:

❯ git diff 6787a8d926ff7fb3f287a4957e21bc93a321d8d4 pechersky/polynomial-notation -U0 --word-diff | grep -F "{+" | grep -v open_locale | grep -v "\[-.*+\}"
{+* Notation to refer to `polynomial R`, as `R[X]` or `R[t]`.+}
{+localized "notation R`[X]`:9000 := polynomial R" in polynomial+}
variables {+{R' : Type*}+} [semiring R] {+[ring R']+} (f g : power_series R) {+(f' g' : power_series R')+}
{+@[simp, norm_cast] lemma coe_sub : ((f' - g' : power_series R') : laurent_series R') = f' - g' :=+}
{+(of_power_series ℤ R').map_sub _ _+}
{+@[simp, norm_cast] lemma coe_neg : ((-f' : power_series R') : laurent_series R') = -f' :=+}
{+(of_power_series ℤ R').map_neg _+}

Changes that don't mention polynomial:

❯ git diff 6787a8d926ff7fb3f287a4957e21bc93a321d8d4 pechersky/polynomial-notation -U0 --word-diff | grep -F "{+" | grep -o "\[-.*+\}" | grep -v polynomial | sort | uniq -c | sort -n -r
      1 [-{α-]{+{S+} : Type*} [semiring [-α]-]{+S]+}  # renaming types in a list big ops file
      1 [-[X]-]{+[mv_power_series.X]+}  # explicit definition identifier in a rewrite so that `[X]` isn't captured

The actual changes:

❯ git diff 6787a8d926ff7fb3f287a4957e21bc93a321d8d4 pechersky/polynomial-notation -U0 --word-diff | grep -F "{+" | grep -o "\[-.*+\}" | sort | uniq -c | sort -n -r
    547 [-polynomial R)-]{+R[X])+}
    273 [-polynomial R}-]{+R[X]}+}
     90 [-polynomial R-]{+R[X]+}
     71 [-polynomial K}-]{+K[X]}+}
     69 [-(polynomial R)-]{+R[X]+}
     56 [-polynomial K)-]{+K[X])+}
     29 [-polynomial R,-]{+R[X],+}
     29 [-(polynomial R))-]{+R[X])+}
     26 [-(polynomial K)-]{+K[X]+}
     23 [-polynomial F)-]{+F[X])+}
     21 [-polynomial S)-]{+S[X])+}
     21 [-polynomial F}-]{+F[X]}+}
     18 [-polynomial A}-]{+A[X]}+}
     15 [-polynomial S}-]{+S[X]}+}
     15 [-polynomial R`-]{+R[X]`+}
     14 [-(polynomial K))-]{+K[X])+}
     13 [-polynomial R),-]{+R[X]),+}
     11 [-polynomial K),-]{+K[X]),+}
     11 [-(polynomial Fq)-]{+Fq[X]+}
     10 [-polynomial α)-]{+α[X])+}
     10 [-polynomial R)-]{+R[X])+} : [-polynomial R-]{+R[X]+}
      9 [-polynomial F).gal-]{+F[X]).gal+}
      9 [-(polynomial R-]{+(R[X]+}
      8 [-polynomial L)-]{+L[X])+}
      8 [-(polynomial R) (polynomial S)]-]{+R[X] S[X]]+}
      7 [-polynomial K-]{+K[X]+}
      7 [-(polynomial K)]-]{+K[X]]+}
      6 [-polynomial R)-]{+R[X])+} {q : [-polynomial R}-]{+R[X]}+}
      6 [-polynomial K)-]{+K[X])+} {q : [-polynomial K}-]{+K[X]}+}
      6 [-polynomial Fq)-]{+Fq[X])+}
      6 [-polynomial A)-]{+A[X])+}
      6 [-(polynomial α))-]{+S[X])+}
      5 [-polynomial T)-]{+T[X])+}
      5 [-polynomial R-]{+R[X]+} →ₗ[R] [-polynomial R-]{+R[X]+}
      5 [-polynomial R).map-]{+R[X]).map+}
      5 [-polynomial R))-]{+R[X]))+}
      5 [-polynomial F,-]{+F[X],+}
      5 [-polynomial 𝕜)-]{+𝕜[X])+}
      5 [-(polynomial K)⁰-]{+K[X]⁰+}
      4 [-polynomial-] (zmod [-p))-]{+p)[X])+}
      4 [-polynomial R).support-]{+R[X]).support+}
      4 [-polynomial R).eval-]{+R[X]).eval+}
      4 [-polynomial R).derivative-]{+R[X]).derivative+}
      4 [-polynomial F-]{+F[X]+}
      4 [-(polynomial R)⁰-]{+R[X]⁰+} ≤ [-(polynomial S)⁰.comap-]{+S[X]⁰.comap+}
      4 [-(polynomial R)ˣ)-]{+R[X]ˣ)+}
      4 [-(polynomial R)}-]{+R[X]}+}
      4 [-(polynomial K)⁰)-]{+K[X]⁰)+} (hq' : q' ∈ [-(polynomial K)⁰),-]{+K[X]⁰),+}
      4 [-(polynomial K))]-]{+K[X])]+}
      3 [-polynomial ℤ}-]{+ℤ[X]}+}
      3 [-polynomial ℤ)-]{+ℤ[X])+}
      3 [-polynomial ℚ}-]{+ℚ[X]}+}
      3 [-polynomial k}-]{+k[X]}+}
      3 [-polynomial k)-]{+k[X])+}
      3 [-polynomial R`.-]{+R[X]`.+}
      3 [-polynomial R-]{+R[X]+} → [-polynomial R-]{+R[X]+}
      3 [-polynomial R-]{+R[X]+} → Prop} (p : [-polynomial R)-]{+R[X])+}
      3 [-polynomial R).sum-]{+R[X]).sum+}
      3 [-polynomial R).eval₂-]{+R[X]).eval₂+}
      3 [-polynomial R).coeff-]{+R[X]).coeff+}
      3 [-polynomial A-]{+A[X]+}
      3 [-(polynomial S)⁰-]{+S[X]⁰+}
      3 [-(polynomial R)`.-]{+R[X]`.+}
      3 [-(polynomial R)),-]{+R[X]),+}
      3 [-(polynomial R')-]{+(R'[X])+}
      3 [-(polynomial K)⁰-]{+K[X]⁰+} ≤ [-(polynomial R)⁰.comap-]{+R[X]⁰.comap+}
      3 [-(polynomial K) (polynomial R)]-]{+K[X] R[X]]+}
      3 [-#(polynomial R)-]{+#R[X]+}
      2 [-polynomial-] (zmod [-p)-]{+p)[X]+}
      2 [-polynomial-] (zmod [-p)),-]{+p)[X]),+}
      2 [-polynomial ℤ-]{+ℤ[X]+}
      2 [-polynomial ℤ),-]{+ℤ[X]),+}
      2 [-polynomial k,-]{+k[X],+}
      2 [-polynomial S-]{+S[X]+}
      2 [-polynomial R}-]{+R[X]}+} (hp : p.monic) (q : [-polynomial R)-]{+R[X])+}
      2 [-polynomial R-]{+R[X]+} →+* [-polynomial R)-]{+R[X])+}
      2 [-polynomial R-]{+R[X]+} → [-polynomial R-]{+R[X]+} → [-polynomial R-]{+R[X]+}
      2 [-polynomial R-]{+R[X]+} → [-polynomial R)-]{+R[X])+}
      2 [-polynomial R)`.-]{+R[X])`.+}
      2 [-polynomial R).separable-]{+R[X]).separable+}
      2 [-polynomial R).roots-]{+R[X]).roots+}
      2 [-polynomial R).nat_trailing_degree-]{+R[X]).nat_trailing_degree+}
      2 [-polynomial R).nat_degree-]{+R[X]).nat_degree+}
      2 [-polynomial R).leading_coeff-]{+R[X]).leading_coeff+}
      2 [-polynomial R)-]{+R[X])+} (t : multiset [-(polynomial R))-]{+R[X])+}
      2 [-polynomial R')-]{+R'[X])+}
      2 [-polynomial K-]{+K[X]+} →ₐ[S] [-polynomial R)-]{+R[X])+}
      2 [-polynomial K-]{+K[X]+} →ₐ[S] L) (hφ : [-(polynomial K)⁰-]{+K[X]⁰+}
      2 [-polynomial K)-]{+K[X])+} (d : [-(polynomial K)⁰)-]{+K[X]⁰)+}
      2 [-polynomial K)).to_finset-]{+K[X])).to_finset+}
      2 [-polynomial K').nat_degree-]{+K'[X]).nat_degree+}
      2 [-polynomial K')-]{+K'[X])+}
      2 [-polynomial F},-]{+F[X]},+}
      2 [-polynomial Fq}-]{+Fq[X]}+} (hb : b ≠ 0) (A : fin n → [-polynomial Fq)-]{+Fq[X])+}
      2 [-polynomial Fq}-]{+Fq[X]}+}
      2 [-polynomial F),-]{+F[X]),+}
      2 [-polynomial F'}-]{+F'[X]}+}
      2 [-(polynomial α)-]{+α[X]+}
      2 [-(polynomial S)-]{+S[X]+}
      2 [-(polynomial R)⁰-]{+R[X]⁰+}
      2 [-(polynomial R)⁰),-]{+R[X]⁰),+}
      2 [-(polynomial R)-]{+R[X]+} {g : [-polynomial R-]{+R[X]+}
      2 [-(polynomial R),-]{+R[X],+}
      2 [-(polynomial R))-]{+R[X])+} (p : [-polynomial R)-]{+R[X])+}
      2 [-(polynomial R))).comp-]{+R[X])).comp+}
      2 [-(polynomial K)⁰-]{+K[X]⁰+} ≤ [-(polynomial R)⁰.comap-]{+R[X]⁰.comap+} φ) (p q : [-polynomial K)-]{+K[X])+}
      2 [-(polynomial F)-]{+F[X]+}
      1 [-{α-]{+{S+} : Type*} [semiring [-α]-]{+S]+}
      1 [-polynomial-] (zmod [-p)).root_set-]{+p)[X]).root_set+}
      1 [-polynomial-] (zmod [-p))).symm-]{+p)[X])).symm+}
      1 [-polynomial-] (matrix n n [-R))-]{+R)[X])+}
      1 [-polynomial-] (adjoin R [-S),-]{+S)[X],+}
      1 [-polynomial-] (R ⧸ [-j))-]{+j)[X])+}
      1 [-polynomial ℤ)-]{+ℤ[X])+} (f : [-polynomial ℤ-]{+ℤ[X]+}
      1 [-polynomial ℚ-]{+ℚ[X]+}
      1 [-polynomial ℚ)-]{+ℚ[X])+}
      1 [-polynomial ℕ)],-]{+ℕ[X])],+}
      1 [-polynomial α}-]{+α[X]}+}
      1 [-polynomial α-]{+α[X]+}
      1 [-polynomial α)-]{+α[X])+} • (1 : matrix n n [-(polynomial α))-]{+α[X])+}
      1 [-polynomial α)-]{+S[X])+}
      1 [-polynomial k-]{+k[X]+}
      1 [-polynomial T}-]{+T[X]}+}
      1 [-polynomial T-]{+T[X]+}
      1 [-polynomial T).root_set-]{+T[X]).root_set+}
      1 [-polynomial T)-]{+T[X])+} : [-polynomial R-]{+R[X]+}
      1 [-polynomial T)-]{+T[X])+} (g : ℕ → T → [-polynomial R)-]{+R[X])+}
      1 [-polynomial S`-]{+S[X]`+}
      1 [-polynomial S)-]{+S[X])+} : p ∈ lifts f ↔ ∃ (q : [-polynomial R),-]{+R[X]),+}
      1 [-polynomial S),-]{+S[X]),+}
      1 [-polynomial R}-]{+R[X]}+} {g : [-polynomial S}-]{+S[X]}+}
      1 [-polynomial R}-]{+R[X]}+} {I : submodule [-(polynomial R) (polynomial R)}-]{+R[X] R[X]}+}
      1 [-polynomial R}-]{+R[X]}+} (q : [-polynomial R)-]{+R[X])+}
      1 [-polynomial R},-]{+R[X]},+}
      1 [-polynomial R`,-]{+R[X]`,+}
      1 [-polynomial R-]{+R[X]+} ⧸ (map C I : ideal [-(polynomial R))-]{+R[X])+}
      1 [-polynomial R-]{+R[X]+} ≃+* [-polynomial S-]{+S[X]+}
      1 [-polynomial R-]{+R[X]+} →ₗ[R] [-polynomial A-]{+A[X]+}
      1 [-polynomial R-]{+R[X]+} →ₐ[R] [-polynomial S`-]{+S[X]`+}
      1 [-polynomial R-]{+R[X]+} →ₐ[R] [-polynomial S-]{+S[X]+} := @aeval _ [-(polynomial S)-]{+S[X]+} _ _ _ (X : [-polynomial S)-]{+S[X])+}
      1 [-polynomial R-]{+R[X]+} →ₐ[R] [-polynomial R-]{+R[X]+}
      1 [-polynomial R-]{+R[X]+} →+* [-polynomial S`-]{+S[X]`+}
      1 [-polynomial R-]{+R[X]+} →+* [-polynomial S-]{+S[X]+}
      1 [-polynomial R-]{+R[X]+} →+* [-polynomial R').ker-]{+R'[X]).ker+}
      1 [-polynomial R-]{+R[X]+} →+* L) (hφ : [-(polynomial R)⁰-]{+R[X]⁰+}
      1 [-polynomial R-]{+R[X]+} →+* A').comp (algebra_map R [-(polynomial R))-]{+R[X])+}
      1 [-polynomial R-]{+R[X]+} →*₀ G₀) (hφ : [-(polynomial R)⁰-]{+R[X]⁰+}
      1 [-polynomial R-]{+R[X]+} →* [-polynomial S`-]{+S[X]`+}
      1 [-polynomial R-]{+R[X]+} → [-polynomial S-]{+S[X]+}
      1 [-polynomial R-]{+R[X]+} → [-polynomial R-]{+R[X]+} →+* [-polynomial R-]{+R[X]+}
      1 [-polynomial R-]{+R[X]+} → Sort*} : Π (p : [-polynomial R),-]{+R[X]),+}
      1 [-polynomial R-]{+R[X]+} × [-polynomial R-]{+R[X]+}
      1 [-polynomial R,-]{+R[X],+} r.is_primitive ∧ (∀ s : [-polynomial R,-]{+R[X],+}
      1 [-polynomial R)^n)-]{+R[X])^n)+}
      1 [-polynomial R)^n))-]{+R[X])^n))+}
      1 [-polynomial R).root_set-]{+R[X]).root_set+}
      1 [-polynomial R).mirror-]{+R[X]).mirror+}
      1 [-polynomial R).map_prod],-]{+R[X]).map_prod],+}
      1 [-polynomial R).erase-]{+R[X]).erase+}
      1 [-polynomial R).comp-]{+R[X]).comp+}
      1 [-polynomial R).coeff-]{+R[X]).coeff+} n)⁻¹ = ((↑u⁻¹ : [-polynomial R).coeff-]{+R[X]).coeff+}
      1 [-polynomial R)-]{+R[X])+} ∉ L) → L.prod.roots = (L : multiset [-(polynomial R)).bind-]{+R[X]).bind+}
      1 [-polynomial R)-]{+R[X])+} {q : [-polynomial R},-]{+R[X]},+}
      1 [-polynomial R)-]{+R[X])+} {g : [-polynomial R}-]{+R[X]}+}
      1 [-polynomial R)-]{+R[X])+} = alg_hom.id R [-(polynomial R)-]{+R[X]+}
      1 [-polynomial R)-]{+R[X])+} = (n : [-polynomial R)-]{+R[X])+}
      1 [-polynomial R)-]{+R[X])+} - (C : R →+* [-polynomial R).map_matrix-]{+R[X]).map_matrix+}
      1 [-polynomial R)-]{+R[X])+} (s : R) : [-polynomial R-]{+R[X]+}
      1 [-polynomial R)-]{+R[X])+} (f : ℕ → R → [-polynomial R)-]{+R[X])+}
      1 [-polynomial R)-]{+R[X])+} (f : [-polynomial R-]{+R[X]+}
      1 [-polynomial R)-]{+R[X])+} ((1 : A) ⊗ₜ[R] (X : [-polynomial R))-]{+R[X]))+}
      1 [-polynomial R))`-]{+R[X]))`+}
      1 [-polynomial R)).is_prime-]{+R[X])).is_prime+}
      1 [-polynomial R)).is_maximal-]{+R[X])).is_maximal+}
      1 [-polynomial R)).add_pow,-]{+R[X])).add_pow,+}
      1 [-polynomial P-]{+P[X]+} →+*[M] [-polynomial Q-]{+Q[X]+}
      1 [-polynomial P-]{+P[X]+} → [-polynomial Q)-]{+Q[X])+}
      1 [-polynomial L}-]{+L[X]}+}
      1 [-polynomial L},-]{+L[X]},+}
      1 [-polynomial K⦄-]{+K[X]⦄+}
      1 [-polynomial K-]{+K[X]+} →+* [-polynomial K).map_matrix-]{+K[X]).map_matrix+}
      1 [-polynomial K-]{+K[X]+} →+* L) (hφ : [-(polynomial K)⁰-]{+K[X]⁰+} ≤ L⁰.comap φ) (p q : [-polynomial K)-]{+K[X])+}
      1 [-polynomial K-]{+K[X]+} →+* L) (hφ : [-(polynomial K)⁰-]{+K[X]⁰+}
      1 [-polynomial K-]{+K[X]+} →*₀ L) (hφ : [-(polynomial K)⁰-]{+K[X]⁰+}
      1 [-polynomial K-]{+K[X]+} × [-polynomial K-]{+K[X]+}
      1 [-polynomial K)`-]{+K[X])`+}
      1 [-polynomial K).nat_degree-]{+K[X]).nat_degree+}
      1 [-polynomial K).degree-]{+K[X]).degree+}
      1 [-polynomial K)-]{+K[X])+} {q} (hq : q ∈ [-(polynomial K)⁰)-]{+K[X]⁰)+}
      1 [-polynomial K)-]{+K[X])+} : [-polynomial K-]{+K[X]+}
      1 [-polynomial K)-]{+K[X])+} (y : [-(polynomial K)⁰)-]{+K[X]⁰)+}
      1 [-polynomial K)-]{+K[X])+} (q : [-(polynomial K)⁰)-]{+K[X]⁰)+}
      1 [-polynomial K)).ker-]{+K[X])).ker+}
      1 [-polynomial K').degree-]{+K'[X]).degree+} < (X ^ p : [-polynomial K').degree,-]{+K'[X]).degree,+}
      1 [-polynomial Fq)-]{+Fq[X])+} (A : fin m.succ → [-polynomial Fq)-]{+Fq[X])+}
      1 [-polynomial F).splits-]{+F[X]).splits+}
      1 [-polynomial F).separable-]{+F[X]).separable+}
      1 [-polynomial F).gal,-]{+F[X]).gal,+}
      1 [-polynomial F).coeff-]{+F[X]).coeff+}
      1 [-polynomial F)-]{+F[X])+} (g : [-polynomial F)-]{+F[X])+}
      1 [-polynomial E,-]{+E[X],+}
      1 [-polynomial E)-]{+E[X])+} (_ : [-polynomial E),-]{+E[X]),+}
      1 [-polynomial A-]{+A[X]+} ≃ₐ[R] (A ⊗[R] [-polynomial R)-]{+R[X])+}
      1 [-polynomial A,-]{+A[X],+}
      1 [-polynomial A)-]{+A[X])+} : A ⊗[R] [-polynomial R-]{+R[X]+}
      1 [-polynomial A'-]{+A'[X]+}
      1 [-polynomial 𝕜}-]{+𝕜[X]}+}
      1 [-`polynomial R`-]{+`R[X]`+}
      1 [-`(polynomial R)ᵐᵒᵖ`-]{+`R[X]ᵐᵒᵖ`+} and [-`polynomial Rᵐᵒᵖ`.-]{+`R[X]ᵐᵒᵖ`.+}
      1 [-[X]-]{+[mv_power_series.X]+}
      1 [-(polynomial α))-]{+α[X])+}
      1 [-(polynomial S)⁰,-]{+S[X]⁰,+}
      1 [-(polynomial S)⁰),-]{+S[X]⁰),+}
      1 [-(polynomial R-]{+(R[X]+} ⧸ (map C P : ideal [-(polynomial R)))-]{+R[X]))+}
      1 [-(polynomial R)⁰-]{+R[X]⁰+} ≤ [-(polynomial S)⁰.comap-]{+S[X]⁰.comap+} φ) (n : [-polynomial R)-]{+R[X])+} (d : [-(polynomial R)⁰)-]{+R[X]⁰)+}
      1 [-(polynomial R)⁰-]{+R[X]⁰+} ≤ L⁰.comap φ) (n : [-polynomial R)-]{+R[X])+} (d : [-(polynomial R)⁰)-]{+R[X]⁰)+}
      1 [-(polynomial R)⁰-]{+R[X]⁰+} ≤ G₀⁰.comap φ) (n : [-polynomial R)-]{+R[X])+} (d : [-(polynomial R)⁰)-]{+R[X]⁰)+}
      1 [-(polynomial R)⁰)-]{+R[X]⁰)+} : taylor r p ∈ [-(polynomial R)⁰-]{+R[X]⁰+}
      1 [-(polynomial R)⁰)-]{+R[X]⁰)+}
      1 [-(polynomial R)ᵐᵒᵖ-]{+R[X]ᵐᵒᵖ+} ≃+* [-polynomial Rᵐᵒᵖ-]{+Rᵐᵒᵖ[X]+}
      1 [-(polynomial R)ˣ)-]{+R[X]ˣ)+} (p : [-polynomial R)-]{+R[X])+}
      1 [-(polynomial R)/P`-]{+R[X]/P`+}
      1 [-(polynomial R)).sum_mem-]{+R[X]).sum_mem+}
      1 [-(polynomial R)).mul_mem_left-]{+R[X]).mul_mem_left+}
      1 [-(polynomial R)).map-]{+R[X]).map+}
      1 [-(polynomial R))-]{+R[X])+} : submodule R [-(polynomial R)-]{+R[X]+}
      1 [-(polynomial R))-]{+R[X])+} (pX : [-polynomial R)-]{+R[X])+}
      1 [-(polynomial R)))ᶜ-]{+R[X]))ᶜ+}
      1 [-(polynomial R))).mp-]{+R[X])).mp+}
      1 [-(polynomial R)))-]{+R[X]))+}
      1 [-(polynomial R')-]{+(R'[X])+} (S' → T') : [-polynomial R'-]{+R'[X]+}
      1 [-(polynomial R')-]{+(R'[X])+} (R' → R') : [-polynomial R'-]{+R'[X]+}
      1 [-(polynomial K)⁰`,-]{+K[X]⁰`,+} `q' ∉ [-(polynomial K)⁰`.-]{+K[X]⁰`.+}
      1 [-(polynomial K)⁰-]{+K[X]⁰+} ≤ L⁰.comap φ) (p q : [-polynomial K)-]{+K[X])+}
      1 [-(polynomial K)ˣ)-]{+(K[X])ˣ)+}
      1 [-(polynomial K)`.-]{+K[X]`.+}
      1 [-(polynomial K)`,-]{+K[X]`,+}
      1 [-(polynomial K)]-]{+K[X]]+} [algebra S L] [algebra S [-(polynomial R)]-]{+R[X]]+}
      1 [-(polynomial K)-]{+K[X]+} →* [-polynomial K).map_pow],-]{+K[X]).map_pow],+}
      1 [-(polynomial K)-]{+K[X]+} _ 0 / algebra_map [-(polynomial K)-]{+K[X]+}
      1 [-(polynomial K)-]{+K[X]+} (fraction_ring [-(polynomial K))-]{+K[X])+}
      1 [-(polynomial K)-]{+K[X]+} (fraction_ring [-(polynomial K))).eq_iff]-]{+K[X])).eq_iff]+}
      1 [-(polynomial K) (polynomial K)]-]{+K[X] K[X]]+} (c : R) (p q : [-polynomial K)-]{+K[X])+}
      1 [-(polynomial K) (polynomial K)]-]{+K[X] K[X]]+}
      1 [-(polynomial Fq)-]{+Fq[X]+} Fqt] [is_fraction_ring [-(polynomial Fq)-]{+Fq[X]+}
      1 [-(polynomial Fq)-]{+Fq[X]+} F] [is_scalar_tower [-(polynomial Fq)-]{+Fq[X]+}
      1 [-(polynomial Fq)-]{+Fq[X]+} F] := integral_closure [-(polynomial Fq)-]{+Fq[X]+}
      1 [-(polynomial Fq)-]{+Fq[X]+} (fraction_ring [-(polynomial Fq))-]{+Fq[X])+}
      1 [-(polynomial Fq))-]{+(Fq[X]))+}
      1 [-(polynomial F)}-]{+F[X]}+}
      1 [-(non_zero_divisors (polynomial Fq))-]{+Fq[X]⁰+}
      1 [-(#(polynomial R))-]{+(#R[X])+}

[jcommelin]

Thanks 🎉

If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.

bors d+

[bors]

✌️ pechersky can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[jcommelin]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests