theorem mem_sup_left {R : Type u_1} [Semiring R] {a b : Subsemiring R} {x : R} : x ∈ a → x ∈ a ⊔ b

theorem mem_sup_right {R : Type u_1} [Semiring R] {a b : Subsemiring R} {x : R} : x ∈ b → x ∈ a ⊔ b

theorem Polynomial.exists_odd_natDegree_monic_irreducible_factor {F : Type u_1} [Field F] {f : Polynomial F} (hf : Odd f.natDegree) : ∃ (g : Polynomial F), Odd g.natDegree ∧ g.Monic ∧ Irreducible g ∧ g ∣ f

theorem Polynomial.exists_root_of_odd_natDegree_irreducible_imp_natDegree_eq_one {F : Type u_1} [Field F] (h : ∀ {g : Polynomial F}, g.Monic → Odd g.natDegree → Irreducible g → g.natDegree = 1) {f : Polynomial F} (hf : Odd f.natDegree) : ∃ (x : F), f.IsRoot x

@[simp]

theorem IsFormallyReal.Subsemiring.sumSq_toAddSubmonoid {T : Type u_2} [CommSemiring T] : (Subsemiring.sumSq T).toAddSubmonoid = AddSubmonoid.sumSq T

theorem IsFormallyReal.AddSubmonoid.IsPointed.sumSq (R : Type u_1) [CommRing R] [IsFormallyReal R] : (AddSubmonoid.sumSq R).IsPointed

theorem IsFormallyReal.Subsemiring.IsPointed.sumSq (R : Type u_1) [CommRing R] [IsFormallyReal R] : (Subsemiring.sumSq R).toAddSubmonoid.IsPointed

@[simp]

theorem Subsemiring.comap_toSubmonoid' {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (Q : Subsemiring S) : (comap f Q).toSubmonoid = Submonoid.comap (↑f) Q.toSubmonoid

@[simp]

theorem Subsemiring.comap_toAddSubmonoid {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (Q : Subsemiring S) : (comap f Q).toAddSubmonoid = AddSubmonoid.comap f.toAddMonoidHom Q.toAddSubmonoid

@[simp]

theorem Subsemiring.map_toSubmonoid' {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (P : Subsemiring R) : (map f P).toSubmonoid = Submonoid.map (↑f) P.toSubmonoid

@[simp]

theorem Subsemiring.map_toAddSubmonoid {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (P : Subsemiring R) : (map f P).toAddSubmonoid = AddSubmonoid.map f.toAddMonoidHom P.toAddSubmonoid

@[simp]

theorem Submodule.map_toAddSubgroup' {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (σ : R →+* S) (M : Type u_3) (M₂ : Type u_4) [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module S M₂] (f : M →ₛₗ[σ] M₂) (p : Submodule R M) [RingHomSurjective σ] : (map f p).toAddSubgroup = AddSubgroup.map f.toAddMonoidHom p.toAddSubgroup

@[simp]

theorem Submodule.comap_toAddSubgroup {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (σ : R →+* S) (M : Type u_3) (M₂ : Type u_4) [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module S M₂] (f : M →ₛₗ[σ] M₂) (q : Submodule S M₂) : (comap f q).toAddSubgroup = AddSubgroup.comap f.toAddMonoidHom q.toAddSubgroup

theorem Ideal.comap_eq_submodule_comap {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (I : Ideal S) : comap f I = Submodule.comap f.toSemilinearMap I

@[simp]

theorem RingHom.toAddMonoidHom_toSemilinearMap {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) : f.toSemilinearMap.toAddMonoidHom = f.toAddMonoidHom

instance instIsSemirealOfNontrivialOfIsFormallyReal_realClosedField {R : Type u_1} [NonAssocSemiring R] [Nontrivial R] [IsFormallyReal R] : IsSemireal R

theorem Subsemiring.IsPreordering.sumSq (R : Type u_1) [CommRing R] [IsSemireal R] : (Subsemiring.sumSq R).IsPreordering

theorem isSemireal_ofIsPreordering {R : Type u_1} [CommRing R] {P : Subsemiring R} (hP : P.IsPreordering) : IsSemireal R

theorem exists_isPreordering_iff_isSemireal {R : Type u_1} [CommRing R] : (∃ (P : Subsemiring R), P.IsPreordering) ↔ IsSemireal R

instance instIsFormallyRealOfIsSemireal_realClosedField {F : Type u_1} [Field F] [IsSemireal F] : IsFormallyReal F

def AlgHom.liftOfRightInverseAux {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : A →ₐ[R] C) (hg : RingHom.ker f ≤ RingHom.ker g) : B →ₐ[R] C

Auxiliary definition used to define liftOfRightInverse

Equations

• f.liftOfRightInverseAux f_inv hf g hg = { toFun := fun (b : B) => g (f_inv b), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem AlgHom.liftOfRightInverseAux_comp_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : A →ₐ[R] C) (hg : RingHom.ker f ≤ RingHom.ker g) (a : A) : (f.liftOfRightInverseAux f_inv hf g hg) (f a) = g a

def AlgHom.liftOfRightInverse {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) : { g : A →ₐ[R] C // RingHom.ker f ≤ RingHom.ker g } ≃ (B →ₐ[R] C)

liftOfRightInverse f hf g hg is the unique R-algebra homomorphism φ

• such that φ.comp f = g (AlgHom.liftOfRightInverse_comp),
• where f : A →ₐ[R] B has a right_inverse f_inv (hf),
• and g : B →ₐ[R] C satisfies hg : f.ker ≤ g.ker.

See AlgHom.eq_liftOfRightInverse for the uniqueness lemma.

   A .
   |  \
 f |   \ g
   |    \
   v     \⌟
   B ----> C
      ∃!φ

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev AlgHom.liftOfSurjective' {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (hf : Function.Surjective ⇑f) : { g : A →ₐ[R] C // RingHom.ker f ≤ RingHom.ker g } ≃ (B →ₐ[R] C)

A non-computable version of AlgHom.liftOfRightInverse for when no computable right inverse is available, that uses Function.surjInv.

Equations

• f.liftOfSurjective' hf = f.liftOfRightInverse (Function.surjInv hf) ⋯

theorem AlgHom.liftOfRightInverse_comp_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : { g : A →ₐ[R] C // RingHom.ker f ≤ RingHom.ker g }) (x : A) : ((f.liftOfRightInverse f_inv hf) g) (f x) = ↑g x

theorem AlgHom.liftOfRightInverse_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : { g : A →ₐ[R] C // RingHom.ker f ≤ RingHom.ker g }) : ((f.liftOfRightInverse f_inv hf) g).comp f = ↑g

theorem AlgHom.liftOfRightInverse_symm {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (φ : B →ₐ[R] C) : ↑((f.liftOfRightInverse f_inv hf).symm φ) = φ.comp f

theorem AlgHom.eq_liftOfRightInverse {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : A →ₐ[R] C) (hg : RingHom.ker f ≤ RingHom.ker g) (h : B →ₐ[R] C) (hh : h.comp f = g) : h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩

theorem AddSubmonoid.IsPointed.neg_one_notMem {R : Type u_1} [Ring R] {S : Subsemiring R} [Nontrivial R] (hS : S.toAddSubmonoid.IsPointed) : -1 ∉ S

theorem Subsemiring.isSpanning_comap {R : Type u_2} {R' : Type u_3} [Ring R] [Ring R'] (f : R →+* R') {S' : Subsemiring R'} (hS' : S'.toAddSubmonoid.IsSpanning) : (comap f S').toAddSubmonoid.IsSpanning

theorem Subsemiring.isSpanning_map {R : Type u_2} {R' : Type u_3} [Ring R] [Ring R'] {f : R →+* R'} {S : Subsemiring R} (hS : S.toAddSubmonoid.IsSpanning) (hf : Function.Surjective ⇑f) : (map f S).toAddSubmonoid.IsSpanning

noncomputable def CommGroup.submonoidPartialOrderEquiv (G : Type u_2) [CommGroup G] : { C : Submonoid G // C.IsMulPointed } ≃ { _o : PartialOrder G // IsOrderedMonoid G }

Equivalence between submonoids with zero support in an abelian group G and partially ordered group structures on G.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AddCommGroup.addSubmonoidPartialOrderEquiv (G : Type u_2) [AddCommGroup G] : { C : AddSubmonoid G // C.IsPointed } ≃ { _o : PartialOrder G // IsOrderedAddMonoid G }

Equivalence between submonoids with zero support in an abelian group G and partially ordered group structures on G.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CommGroup.submonoidPartialOrderEquiv_apply {G : Type u_2} [CommGroup G] (C : Submonoid G) (h : C.IsMulPointed) : ↑((submonoidPartialOrderEquiv G) ⟨C, h⟩) = PartialOrder.ofSubmonoid h

@[simp]

theorem AddCommGroup.addSubmonoidPartialOrderEquiv_apply {G : Type u_2} [AddCommGroup G] (C : AddSubmonoid G) (h : C.IsPointed) : ↑((addSubmonoidPartialOrderEquiv G) ⟨C, h⟩) = PartialOrder.ofAddSubmonoid h

@[simp]

theorem CommGroup.submonoidPartialOrderEquiv_symm_apply {G : Type u_2} [CommGroup G] (o : PartialOrder G) (h : IsOrderedMonoid G) : ↑((submonoidPartialOrderEquiv G).symm ⟨o, h⟩) = Submonoid.oneLE G

@[simp]

theorem AddCommGroup.addSubmonoidPartialOrderEquiv_symm_apply {G : Type u_2} [AddCommGroup G] (o : PartialOrder G) (h : IsOrderedAddMonoid G) : ↑((addSubmonoidPartialOrderEquiv G).symm ⟨o, h⟩) = AddSubmonoid.nonneg G

noncomputable def CommGroup.submonoidLinearOrderEquiv (G : Type u_2) [CommGroup G] : { C : Submonoid G // C.IsMulPointed ∧ C.IsMulSpanning } ≃ { _o : LinearOrder G // IsOrderedMonoid G }

Equivalence between maximal submonoids with zero support in an abelian group G and linearly ordered group structures on G.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AddCommGroup.addSubmonoidLinearOrderEquiv (G : Type u_2) [AddCommGroup G] : { C : AddSubmonoid G // C.IsPointed ∧ C.IsSpanning } ≃ { _o : LinearOrder G // IsOrderedAddMonoid G }

Equivalence between maximal submonoids with zero support in an abelian group G and linearly ordered group structures on G.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CommGroup.submonoidLinearOrderEquiv_apply {G : Type u_2} [CommGroup G] (C : Submonoid G) (h : C.IsMulPointed ∧ C.IsMulSpanning) : ↑((submonoidLinearOrderEquiv G) ⟨C, h⟩) = LinearOrder.ofSubmonoid ⋯ ⋯

@[simp]

theorem AddCommGroup.addSubmonoidLinearOrderEquiv_apply {G : Type u_2} [AddCommGroup G] (C : AddSubmonoid G) (h : C.IsPointed ∧ C.IsSpanning) : ↑((addSubmonoidLinearOrderEquiv G) ⟨C, h⟩) = LinearOrder.ofAddSubmonoid ⋯ ⋯

@[simp]

theorem CommGroup.submonoidLinearOrderEquiv_symm_apply {G : Type u_2} [CommGroup G] (l : LinearOrder G) (h : IsOrderedMonoid G) : ↑((submonoidLinearOrderEquiv G).symm ⟨l, h⟩) = Submonoid.oneLE G

@[simp]

theorem AddCommGroup.addSubmonoidLinearOrderEquiv_symm_apply {G : Type u_2} [AddCommGroup G] (l : LinearOrder G) (h : IsOrderedAddMonoid G) : ↑((addSubmonoidLinearOrderEquiv G).symm ⟨l, h⟩) = AddSubmonoid.nonneg G

noncomputable def Ring.isPointedPartialOrderEquiv (R : Type u_1) [Ring R] : { C : Subsemiring R // C.toAddSubmonoid.IsPointed } ≃ { _o : PartialOrder R // IsOrderedRing R }

Equivalence between subsemirings with zero support in a ring R and partially ordered ring structures on R.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ring.isPointedPartialOrderEquiv_apply {R : Type u_1} [Ring R] (C : Subsemiring R) (h : C.toAddSubmonoid.IsPointed) : ↑((isPointedPartialOrderEquiv R) ⟨C, h⟩) = PartialOrder.ofAddSubmonoid h

@[simp]

theorem Ring.isPointedPartialOrderEquiv_symm_apply {R : Type u_1} [Ring R] (o : PartialOrder R) (h : IsOrderedRing R) : ↑((isPointedPartialOrderEquiv R).symm ⟨o, h⟩) = Subsemiring.nonneg R

noncomputable def Ring.isPointedLinearOrderEquiv (R : Type u_1) [Ring R] : { C : Subsemiring R // C.toAddSubmonoid.IsPointed ∧ C.toAddSubmonoid.IsSpanning } ≃ { _o : LinearOrder R // IsOrderedRing R }

Equivalence between maximal subsemirings with zero support in a ring R and linearly ordered ring structures on R.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ring.isPointedLinearOrderEquiv_apply {R : Type u_1} [Ring R] (C : Subsemiring R) (h : C.toAddSubmonoid.IsPointed ∧ C.toAddSubmonoid.IsSpanning) : ↑((isPointedLinearOrderEquiv R) ⟨C, h⟩) = LinearOrder.ofAddSubmonoid ⋯ ⋯

@[simp]

theorem Ring.isPointedLinearOrderEquiv_symm_apply {R : Type u_1} [Ring R] (o : LinearOrder R) (h : IsOrderedRing R) : ↑((isPointedLinearOrderEquiv R).symm ⟨o, h⟩) = Subsemiring.nonneg R

theorem estimate {F : Type u_2} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {f : Polynomial F} (hdeg : f.natDegree ≠ 0) {x : F} (hx : 1 ≤ x) : x ^ (f.natDegree - 1) * (f.leadingCoeff * x - ↑f.natDegree * (Finset.image (fun (x : ℕ) => |f.coeff x|) (Finset.range f.natDegree)).max' ⋯) ≤ Polynomial.eval x f

theorem eventually_pos {F : Type u_2} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {f : Polynomial F} (hdeg : f.natDegree ≠ 0) (hf : 0 < f.leadingCoeff) : ∃ (y : F), ∀ (x : F), y < x → 0 < Polynomial.eval x f

theorem estimate2 {F : Type u_2} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {f : Polynomial F} (hdeg : Odd f.natDegree) {x : F} (hx : x ≤ -1) : Polynomial.eval x f ≤ x ^ (f.natDegree - 1) * (f.leadingCoeff * x + ↑f.natDegree * (Finset.image (fun (x : ℕ) => |f.coeff x|) (Finset.range f.natDegree)).max' ⋯)

theorem eventually_neg {F : Type u_2} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {f : Polynomial F} (hdeg : Odd f.natDegree) (hf : 0 < f.leadingCoeff) : ∃ (y : F), ∀ x < y, Polynomial.eval x f < 0

theorem sign_change {F : Type u_2} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {f : Polynomial F} (hdeg : Odd f.natDegree) : ∃ (x : F) (y : F), Polynomial.eval x f < 0 ∧ 0 < Polynomial.eval y f

def Localization.recOnSubsingleton {M : Type u_2} [CommMonoid M] {S : Submonoid M} {r : Localization S → Sort u_3} [h : ∀ (a : M) (b : ↥S), Subsingleton (r (mk a b))] (x : Localization S) (f : (a : M) → (b : ↥S) → r (mk a b)) : r x

Copy of Quotient.recOnSubsingleton for Localization

Equations

• x.recOnSubsingleton f = Quotient.recOnSubsingleton' x fun (t : M × ↥S) => Prod.rec (fun (x : M) (x_1 : ↥S) => f x x_1) t

def AddLocalization.recOnSubsingleton {M : Type u_2} [AddCommMonoid M] {S : AddSubmonoid M} {r : AddLocalization S → Sort u_3} [h : ∀ (a : M) (b : ↥S), Subsingleton (r (mk a b))] (x : AddLocalization S) (f : (a : M) → (b : ↥S) → r (mk a b)) : r x

Copy of Quotient.recOnSubsingleton for AddLocalization

Equations

• x.recOnSubsingleton f = Quotient.recOnSubsingleton' x fun (t : M × ↥S) => Prod.rec (fun (x : M) (x_1 : ↥S) => f x x_1) t