ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>Fintype σ<VAR>n : ℕ<VAR>DecidableEq σ<VAR>Nontrivial R<GOAL>(MvPolynomial.esymm σ R n).support = (Finset.powersetCard n Finset.univ).biUnion fun t => (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>Fintype σ<VAR>n : ℕ<VAR>DecidableEq σ<VAR>Nontrivial R<GOAL>(MvPolynomial.esymm σ R n).support = (Finset.powersetCard n Finset.univ).biUnion fun t => {∑ i ∈ t, Finsupp.single i 1}
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>Fintype σ<VAR>n : ℕ<VAR>DecidableEq σ<VAR>Nontrivial R<GOAL>(MvPolynomial.esymm σ R n).support = Finset.image (fun t => ∑ i ∈ t, Finsupp.single i 1) (Finset.powersetCard n Finset.univ)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>Fintype σ<VAR>Nontrivial R<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>hn : n ≤ Fintype.card σ<GOAL>(MvPolynomial.esymm σ R n).degrees = Finset.univ.val
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>Fintype σ<VAR>n : ℕ<GOAL>MvPolynomial.psum σ R n = ∑ i : σ, MvPolynomial.X i ^ n
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>Fintype σ<GOAL>MvPolynomial.psum σ R 0 = ↑(Fintype.card σ)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>Fintype σ<GOAL>MvPolynomial.psum σ R 1 = ∑ i : σ, MvPolynomial.X i
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>CommSemiring R<VAR>Fintype σ<VAR>Fintype τ<VAR>n : ℕ<VAR>e : σ ≃ τ<GOAL>(MvPolynomial.rename ⇑e) (MvPolynomial.psum σ R n) = MvPolynomial.psum τ R n
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>Fintype σ<VAR>n : ℕ<GOAL>(MvPolynomial.psum σ R n).IsSymmetric
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>c : RingCon R<GOAL>Setoid.r = ⇑c
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>c : RingCon R<GOAL>⇑c.toCon = ⇑c
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>c : RingCon R<VAR>x : R<GOAL>c x x
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>c : RingCon R<VAR>x y : R<GOAL>c x y → c y x
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>c : RingCon R<VAR>x y z : R<GOAL>c x y → c y z → c x z
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>c : RingCon R<VAR>w x y z : R<GOAL>c w x → c y z → c (w + y) (x + z)
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>c : RingCon R<VAR>w x y z : R<GOAL>c w x → c y z → c (w * y) (x * z)
<VAR>S : Type u_3<VAR>AddGroup S<VAR>Mul S<VAR>t : RingCon S<VAR>a b c d : S<VAR>h : t a b<VAR>h' : t c d<GOAL>t (a - c) (b - d)
<VAR>S : Type u_3<VAR>AddGroup S<VAR>Mul S<VAR>t : RingCon S<VAR>a b : S<VAR>h : t a b<GOAL>t (-a) (-b)
<VAR>S : Type u_3<VAR>AddGroup S<VAR>Mul S<VAR>t : RingCon S<VAR>m : ℕ<VAR>x y : S<VAR>hx : t x y<GOAL>t (m • x) (m • y)
<VAR>S : Type u_3<VAR>AddGroup S<VAR>Mul S<VAR>t : RingCon S<VAR>z : ℤ<VAR>x y : S<VAR>hx : t x y<GOAL>t (z • x) (z • y)
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>s : Con R<VAR>h : ∀ {w x y z : R}, Setoid.r w x → Setoid.r y z → Setoid.r (w + y) (x + z)<VAR>a b : R<GOAL>{ toCon := s, add' := h } a b ↔ s a b
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>c d : RingCon R<VAR>H : ⇑c = ⇑d<GOAL>c = d
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>c d : RingCon R<VAR>H : ∀ (x y : R), c x y ↔ d x y<GOAL>c = d
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>c : RingCon R<VAR>x : R<GOAL>Quot.mk (⇑c) x = ↑x
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>c : RingCon R<VAR>a b : R<GOAL>↑a = ↑b ↔ c a b
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>c : RingCon R<VAR>x y : R<GOAL>↑(x + y) = ↑x + ↑y
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>c : RingCon R<VAR>x y : R<GOAL>↑(x * y) = ↑x * ↑y
<VAR>R : Type u_2<VAR>AddZeroClass R<VAR>Mul R<VAR>c : RingCon R<GOAL>↑0 = 0
<VAR>R : Type u_2<VAR>Add R<VAR>MulOneClass R<VAR>c : RingCon R<GOAL>↑1 = 1
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>Add R<VAR>MulOneClass R<VAR>SMul α R<VAR>IsScalarTower α R R<VAR>c : RingCon R<VAR>a : α<VAR>x : R<GOAL>↑(a • x) = a • ↑x
<VAR>R : Type u_2<VAR>AddGroup R<VAR>Mul R<VAR>c : RingCon R<VAR>x : R<GOAL>↑(-x) = -↑x
<VAR>R : Type u_2<VAR>AddGroup R<VAR>Mul R<VAR>c : RingCon R<VAR>x y : R<GOAL>↑(x - y) = ↑x - ↑y
<VAR>R : Type u_2<VAR>AddGroup R<VAR>Mul R<VAR>c : RingCon R<VAR>z : ℤ<VAR>x : R<GOAL>↑(z • x) = z • ↑x
<VAR>R : Type u_2<VAR>AddMonoid R<VAR>Mul R<VAR>c : RingCon R<VAR>n : ℕ<VAR>x : R<GOAL>↑(n • x) = n • ↑x
<VAR>R : Type u_2<VAR>Add R<VAR>Monoid R<VAR>c : RingCon R<VAR>x : R<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>R : Type u_2<VAR>AddMonoidWithOne R<VAR>Mul R<VAR>c : RingCon R<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>R : Type u_2<VAR>AddGroupWithOne R<VAR>Mul R<VAR>c : RingCon R<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>c d : RingCon R<GOAL>c ≤ d ↔ ∀ {x y : R}, c x y → d x y
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>S : Set (RingCon R)<GOAL>(sInf S).toSetoid = sInf ((fun x => x.toSetoid) '' S)
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>S : Set (RingCon R)<GOAL>⇑(sInf S) = sInf (DFunLike.coe '' S)
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>ι : Sort u_3<VAR>f : ι → RingCon R<GOAL>⇑(iInf f) = ⨅ i, ⇑(f i)
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<GOAL>⇑⊤ = ⊤
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<GOAL>⇑⊥ = Eq
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>c d : RingCon R<GOAL>⇑(c ⊓ d) = ⇑c ⊓ ⇑d
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>c d : RingCon R<VAR>x y : R<GOAL>(c ⊓ d) x y ↔ c x y ∧ d x y
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>r : R → R → Prop<GOAL>ringConGen r = sInf {s | ∀ (x y : R), r x y → s x y}
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>r : R → R → Prop<VAR>c : RingCon R<VAR>h : ∀ (x y : R), r x y → c x y<GOAL>ringConGen r ≤ c
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>r s : R → R → Prop<VAR>h : ∀ (x y : R), r x y → s x y<GOAL>ringConGen r ≤ ringConGen s
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>c : RingCon R<GOAL>ringConGen ⇑c = c
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>r : R → R → Prop<GOAL>ringConGen ⇑(ringConGen r) = ringConGen r
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>c d : RingCon R<GOAL>c ⊔ d = ringConGen fun x y => c x y ∨ d x y
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>c d : RingCon R<GOAL>c ⊔ d = ringConGen (⇑c ⊔ ⇑d)
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>S : Set (RingCon R)<GOAL>sSup S = ringConGen fun x y => ∃ c ∈ S, c x y
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>S : Set (RingCon R)<GOAL>sSup S = ringConGen (sSup (DFunLike.coe '' S))
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R[X]<VAR>P : Ideal R<VAR>hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P<GOAL>Polynomial.map (Ideal.Quotient.mk P) f = Polynomial.C ((Ideal.Quotient.mk P) f.leadingCoeff) * Polynomial.X ^ f.natDegree
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>q : R[X]<VAR>c : (R ⧸ P)[X]<VAR>hq : Polynomial.map (Ideal.Quotient.mk P) q = c * Polynomial.X ^ n<VAR>hc0 : c.degree = 0<GOAL>n ≤ q.natDegree
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>P : Ideal R<VAR>q : R[X]<VAR>c : (R ⧸ P)[X]<VAR>hq : Polynomial.map (Ideal.Quotient.mk P) q = c * Polynomial.X ^ n<VAR>hn0 : n ≠ 0<GOAL>Polynomial.eval 0 q ∈ P
<VAR>R : Type u_1<VAR>CommRing R<VAR>p q : R[X]<VAR>hu : (p * q).IsPrimitive<VAR>hpm : p.natDegree = 0<GOAL>IsUnit p
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>f : R[X]<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>hfl : f.leadingCoeff ∉ P<VAR>hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P<VAR>hfd0 : 0 < f.degree<VAR>h0 : f.coeff 0 ∉ P ^ 2<VAR>hu : f.IsPrimitive<GOAL>Irreducible f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>x : S<GOAL>(Algebra.norm R) x = LinearMap.det ((Algebra.lmul R S) x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>h : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)<VAR>x : S<GOAL>(Algebra.norm R) x = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>h : ¬Module.Finite R S<VAR>x : S<GOAL>(Algebra.norm R) x = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>ι : Type w<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι R S<VAR>s : S<GOAL>(Algebra.norm R) s = ((Algebra.leftMulMatrix b) s).det
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>ι : Type w<VAR>Fintype ι<VAR>b : Basis ι R S<VAR>x : R<GOAL>(Algebra.norm R) ((algebraMap R S) x) = x ^ Fintype.card ι
<VAR>K : Type u_4<VAR>Field K<VAR>L : Type u_7<VAR>Ring L<VAR>Algebra K L<VAR>x : K<GOAL>(Algebra.norm K) ((algebraMap K L) x) = x ^ FiniteDimensional.finrank K L
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_3<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>a : R<VAR>m : ↥M<GOAL>MvPolynomial.C (IsLocalization.mk' S a m) = IsLocalization.mk' (MvPolynomial σ S) (MvPolynomial.C a) ⟨MvPolynomial.C ↑m, ⋯⟩
<VAR>R : Type u_2<VAR>CommRing R<VAR>S : Type u_3<VAR>CommRing S<VAR>Algebra R S<VAR>r : R<VAR>IsLocalization.Away r S<VAR>p : MvPolynomial Unit R<GOAL>(IsLocalization.Away.auxHom S r) ((Ideal.Quotient.mk (Ideal.span {MvPolynomial.C r * MvPolynomial.X () - 1})) p) = (MvPolynomial.aeval fun x => IsLocalization.Away.invSelf r) p
<VAR>R : Type u_2<VAR>CommRing R<VAR>S : Type u_3<VAR>CommRing S<VAR>Algebra R S<VAR>r : R<VAR>IsLocalization.Away r S<GOAL>(IsLocalization.Away.auxHom S r).comp (IsLocalization.Away.auxInv S r) = RingHom.id S
<VAR>R : Type u_2<VAR>CommRing R<VAR>S : Type u_3<VAR>CommRing S<VAR>Algebra R S<VAR>r : R<VAR>IsLocalization.Away r S<GOAL>(IsLocalization.Away.auxInv S r).comp (IsLocalization.Away.auxHom S r).toRingHom = RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {MvPolynomial.C r * MvPolynomial.X () - 1})
<VAR>R : Type u_2<VAR>CommRing R<VAR>S : Type u_3<VAR>CommRing S<VAR>Algebra R S<VAR>r : R<VAR>IsLocalization.Away r S<VAR>p : MvPolynomial Unit R<GOAL>(IsLocalization.Away.mvPolynomialQuotientEquiv S r) ((Ideal.Quotient.mk (Ideal.span {MvPolynomial.C r * MvPolynomial.X () - 1})) p) = (MvPolynomial.aeval fun x => IsLocalization.Away.invSelf r) p
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>f : R[X]<VAR>self : IsAdjoinRoot S f<GOAL>Function.Surjective ⇑self.map
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>f : R[X]<VAR>self : IsAdjoinRoot S f<GOAL>algebraMap R S = self.map.comp Polynomial.C
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>f : R[X]<VAR>self : IsAdjoinRoot S f<GOAL>RingHom.ker self.map = Ideal.span {f}
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>f : R[X]<VAR>self : IsAdjoinRootMonic S f<GOAL>f.Monic
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRoot S f<VAR>Subsingleton R<GOAL>Subsingleton S
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRoot S f<VAR>x : R<GOAL>(algebraMap R S) x = h.map (Polynomial.C x)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRoot S f<VAR>p : R[X]<GOAL>p ∈ RingHom.ker h.map ↔ f ∣ p
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRoot S f<VAR>p : R[X]<GOAL>h.map p = 0 ↔ f ∣ p
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRoot S f<GOAL>h.map Polynomial.X = h.root
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRoot S f<GOAL>h.map f = 0
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRoot S f<VAR>p : R[X]<GOAL>(Polynomial.aeval h.root) p = h.map p
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRoot S f<GOAL>(Polynomial.aeval h.root) f = 0
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRoot S f<VAR>x : S<GOAL>h.map (h.repr x) = x
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRoot S f<GOAL>h.repr 0 ∈ Ideal.span {f}
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRoot S f<VAR>x y : S<GOAL>h.repr (x + y) - (h.repr x + h.repr y) ∈ Ideal.span {f}
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h h' : IsAdjoinRoot S f<VAR>eq : ∀ (x : R[X]), h.map x = h'.map x<GOAL>h = h'
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h h' : IsAdjoinRoot S f<VAR>eq : h.root = h'.root<GOAL>h = h'
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>i : R →+* T<VAR>x : T<VAR>hx : Polynomial.eval₂ i x f = 0<VAR>h : IsAdjoinRoot S f<VAR>z : S<VAR>w : R[X]<VAR>hzw : h.map w = z<GOAL>Polynomial.eval₂ i x (h.repr z) = Polynomial.eval₂ i x w
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>i : R →+* T<VAR>x : T<VAR>hx : Polynomial.eval₂ i x f = 0<VAR>h : IsAdjoinRoot S f<VAR>z : R[X]<GOAL>(IsAdjoinRoot.lift i x hx h) (h.map z) = Polynomial.eval₂ i x z
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>i : R →+* T<VAR>x : T<VAR>hx : Polynomial.eval₂ i x f = 0<VAR>h : IsAdjoinRoot S f<GOAL>(IsAdjoinRoot.lift i x hx h) h.root = x
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>i : R →+* T<VAR>x : T<VAR>hx : Polynomial.eval₂ i x f = 0<VAR>h : IsAdjoinRoot S f<VAR>a : R<GOAL>(IsAdjoinRoot.lift i x hx h) ((algebraMap R S) a) = i a
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>i : R →+* T<VAR>x : T<VAR>hx : Polynomial.eval₂ i x f = 0<VAR>h : IsAdjoinRoot S f<VAR>g : S →+* T<VAR>hmap : ∀ (a : R), g ((algebraMap R S) a) = i a<VAR>hroot : g h.root = x<VAR>a : S<GOAL>g a = (IsAdjoinRoot.lift i x hx h) a
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>i : R →+* T<VAR>x : T<VAR>hx : Polynomial.eval₂ i x f = 0<VAR>h : IsAdjoinRoot S f<VAR>g : S →+* T<VAR>hmap : ∀ (a : R), g ((algebraMap R S) a) = i a<VAR>hroot : g h.root = x<GOAL>g = IsAdjoinRoot.lift i x hx h
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>x : T<VAR>Algebra R T<VAR>hx' : (Polynomial.aeval x) f = 0<VAR>h : IsAdjoinRoot S f<GOAL>↑(IsAdjoinRoot.liftHom x hx' h) = IsAdjoinRoot.lift (algebraMap R T) x hx' h
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>x : T<VAR>Algebra R T<VAR>hx' : (Polynomial.aeval x) f = 0<VAR>h : IsAdjoinRoot S f<VAR>z : S<GOAL>(IsAdjoinRoot.lift (algebraMap R T) x hx' h) z = (IsAdjoinRoot.liftHom x hx' h) z
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>x : T<VAR>Algebra R T<VAR>hx' : (Polynomial.aeval x) f = 0<VAR>h : IsAdjoinRoot S f<VAR>z : R[X]<GOAL>(IsAdjoinRoot.liftHom x hx' h) (h.map z) = (Polynomial.aeval x) z
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>x : T<VAR>Algebra R T<VAR>hx' : (Polynomial.aeval x) f = 0<VAR>h : IsAdjoinRoot S f<GOAL>(IsAdjoinRoot.liftHom x hx' h) h.root = x
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>x : T<VAR>Algebra R T<VAR>hx' : (Polynomial.aeval x) f = 0<VAR>h : IsAdjoinRoot S f<VAR>g : S →ₐ[R] T<VAR>hroot : g h.root = x<GOAL>g = IsAdjoinRoot.liftHom x hx' h
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<GOAL>(AdjoinRoot.isAdjoinRoot f).map = AdjoinRoot.mk f
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<VAR>hf : f.Monic<GOAL>(AdjoinRoot.isAdjoinRootMonic f hf).map = AdjoinRoot.mk f
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<GOAL>(AdjoinRoot.isAdjoinRoot f).root = AdjoinRoot.root f
<VAR>R : Type u<VAR>CommRing R<VAR>f : R[X]<VAR>hf : f.Monic<GOAL>(AdjoinRoot.isAdjoinRootMonic f hf).root = AdjoinRoot.root f
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>g : R[X]<GOAL>h.map (g %ₘ f) = h.map g
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>g : R[X]<GOAL>h.repr (h.map g) %ₘ f = g %ₘ f
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>g : R[X]<GOAL>h.modByMonicHom (h.map g) = g %ₘ f
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>x : S<GOAL>h.map (h.modByMonicHom x) = x
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>n : ℕ<VAR>hdeg : n < f.natDegree<GOAL>h.modByMonicHom (h.root ^ n) = Polynomial.X ^ n
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>hdeg : 1 < f.natDegree<GOAL>h.modByMonicHom h.root = Polynomial.X
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>i : Fin f.natDegree<GOAL>h.basis i = h.root ^ ↑i
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>Nontrivial S<VAR>h : IsAdjoinRootMonic S f<GOAL>0 < f.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>Nontrivial S<VAR>h : IsAdjoinRootMonic S f<GOAL>f.natDegree ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<GOAL>h.powerBasis.dim = f.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<GOAL>h.powerBasis.basis = h.basis
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<GOAL>h.powerBasis.gen = h.root
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>x : S<VAR>i : Fin f.natDegree<GOAL>(h.basis.repr x) i = (h.modByMonicHom x).coeff ↑i
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>hdeg : 1 < f.natDegree<GOAL>h.basis ⟨1, hdeg⟩ = h.root
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>T : Type u_1<VAR>AddCommGroup T<VAR>Module R T<VAR>h : IsAdjoinRootMonic S f<VAR>g : R[X] →ₗ[R] T<GOAL>∀ (a : S), (h.liftPolyₗ g) a = g (h.modByMonicHom a)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>z : S<VAR>i : ℕ<VAR>hi : i < f.natDegree<GOAL>h.coeff z i = (h.basis.repr z) ⟨i, hi⟩
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>z : S<VAR>i : Fin f.natDegree<GOAL>h.coeff z ↑i = (h.basis.repr z) i
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>z : S<VAR>i : ℕ<VAR>hi : f.natDegree ≤ i<GOAL>h.coeff z i = 0
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>z : S<VAR>i : ℕ<GOAL>h.coeff z i = if hi : i < f.natDegree then (h.basis.repr z) ⟨i, hi⟩ else 0
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>n : ℕ<VAR>hn : n < f.natDegree<GOAL>h.coeff (h.root ^ n) = Pi.single n 1
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>Nontrivial S<VAR>h : IsAdjoinRootMonic S f<GOAL>h.coeff 1 = Pi.single 0 1
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>hdeg : 1 < f.natDegree<GOAL>h.coeff h.root = Pi.single 1 1
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>Nontrivial S<VAR>h : IsAdjoinRootMonic S f<VAR>x : R<GOAL>h.coeff ((algebraMap R S) x) = Pi.single 0 x
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>x y : S<VAR>hxy : ∀ i < f.natDegree, h.coeff x i = h.coeff y i<GOAL>x = y
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>x y : S<GOAL>x = y ↔ ∀ i < f.natDegree, h.coeff x i = h.coeff y i
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<GOAL>Function.Injective ⇑h.coeff
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>f : R[X]<VAR>Algebra R S<VAR>h : IsAdjoinRootMonic S f<GOAL>IsIntegral R h.root
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>f : R[X]<VAR>h : IsAdjoinRoot S f<VAR>x : S<GOAL>(IsAdjoinRoot.lift (algebraMap R S) h.root ⋯ h) x = x
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>f : R[X]<VAR>h : IsAdjoinRoot S f<GOAL>IsAdjoinRoot.lift (algebraMap R S) h.root ⋯ h = RingHom.id S
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>f : R[X]<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>h : IsAdjoinRoot S f<VAR>h' : IsAdjoinRoot T f<VAR>z : R[X]<GOAL>(h.aequiv h') (h.map z) = h'.map z
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>f : R[X]<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>h : IsAdjoinRoot S f<VAR>h' : IsAdjoinRoot T f<GOAL>(h.aequiv h') h.root = h'.root
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>f : R[X]<VAR>h : IsAdjoinRoot S f<GOAL>h.aequiv h = AlgEquiv.refl
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>f : R[X]<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>h : IsAdjoinRoot S f<VAR>h' : IsAdjoinRoot T f<GOAL>(h.aequiv h').symm = h'.aequiv h
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>f : R[X]<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>U : Type u_2<VAR>CommRing U<VAR>h : IsAdjoinRoot S f<VAR>h' : IsAdjoinRoot T f<VAR>i : R →+* U<VAR>x : U<VAR>hx : Polynomial.eval₂ i x f = 0<VAR>z : S<GOAL>(IsAdjoinRoot.lift i x hx h') ((h.aequiv h') z) = (IsAdjoinRoot.lift i x hx h) z
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>f : R[X]<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>U : Type u_2<VAR>CommRing U<VAR>Algebra R U<VAR>h : IsAdjoinRoot S f<VAR>h' : IsAdjoinRoot T f<VAR>x : U<VAR>hx : (Polynomial.aeval x) f = 0<VAR>z : S<GOAL>(IsAdjoinRoot.liftHom x hx h') ((h.aequiv h') z) = (IsAdjoinRoot.liftHom x hx h) z
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>f : R[X]<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>U : Type u_2<VAR>CommRing U<VAR>Algebra R U<VAR>h : IsAdjoinRoot S f<VAR>h' : IsAdjoinRoot T f<VAR>h'' : IsAdjoinRoot U f<VAR>x : S<GOAL>(h'.aequiv h'') ((h.aequiv h') x) = (h.aequiv h'') x
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>f : R[X]<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>U : Type u_2<VAR>CommRing U<VAR>Algebra R U<VAR>h : IsAdjoinRoot S f<VAR>h' : IsAdjoinRoot T f<VAR>h'' : IsAdjoinRoot U f<GOAL>(h.aequiv h').trans (h'.aequiv h'') = h.aequiv h''
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>f : R[X]<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>h : IsAdjoinRoot S f<VAR>e : S ≃ₐ[R] T<GOAL>∀ (a : R[X]), (h.ofEquiv e).map a = e (h.map a)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>f : R[X]<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>h : IsAdjoinRoot S f<VAR>e : S ≃ₐ[R] T<GOAL>(h.ofEquiv e).root = e h.root
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>f : R[X]<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>U : Type u_2<VAR>CommRing U<VAR>Algebra R U<VAR>h : IsAdjoinRoot S f<VAR>h' : IsAdjoinRoot T f<VAR>e : T ≃ₐ[R] U<GOAL>h.aequiv (h'.ofEquiv e) = (h.aequiv h').trans e