Documentation

RealClosedField.Prereqs

source
theorem mem_sup_of_mem_left {R : Type u_1} [Semiring R] {a b : Subsemiring R} {x : R} :
x ∈ a → x ∈ a ⊔ b
source
theorem mem_sup_of_mem_right {R : Type u_1} [Semiring R] {a b : Subsemiring R} {x : R} :
x ∈ b → x ∈ a ⊔ b
source
theorem Ideal.irreducible_of_isMaximal_span_singleton {R : Type u_1} [CommRing R] [IsDomain R] {m : R} (hm : m ≠ 0) (hmax : (span {m}).IsMaximal) :
Irreducible m
source
theorem Ideal.span_singleton_irreducible {R : Type u_1} [CommRing R] [IsPrincipalIdealRing R] [IsDomain R] {m : R} (hm : m ≠ 0) :
(span {m}).IsMaximal ↔ Irreducible m
source
theorem Ideal.Quotient.isField_of_irreducible {R : Type u_1} [CommRing R] [IsPrincipalIdealRing R] {m : R} (hirr : Irreducible m) :
IsField (R ⧸ span {m})
source
theorem Ideal.Quotient.irreducible_of_isField {R : Type u_1} [CommRing R] [IsDomain R] {m : R} (hm : m ≠ 0) (hf : IsField (R ⧸ span {m})) :
Irreducible m
source
theorem Ideal.Quotient.irreducible_iff_isField {R : Type u_1} [CommRing R] [IsPrincipalIdealRing R] [IsDomain R] {m : R} (hm : m ≠ 0) :
Irreducible m ↔ IsField (R ⧸ span {m})
source
theorem Polynomial.natDegree_eq_one_iff_degree_eq_one {R : Type u_1} [Semiring R] {p : Polynomial R} :
p.degree = 1 ↔ p.natDegree = 1
source
theorem Polynomial.natDegree_eq_iff_degree_eq_of_atLeastTwo {R : Type u_1} [Semiring R] {p : Polynomial R} {n : ℕ} [n.AtLeastTwo] :
p.degree = ↑n ↔ p.natDegree = n
source
@[simp]
theorem Polynomial.natDegree_add_one {R : Type u_1} [Semiring R] {p : Polynomial R} :
(p + 1).natDegree = p.natDegree
source
@[simp]
theorem Polynomial.natDegree_one_add {R : Type u_1} [Semiring R] {p : Polynomial R} :
(1 + p).natDegree = p.natDegree
source
@[simp]
theorem Polynomial.natDegree_normalize {R : Type u_1} [Field R] {p : Polynomial R} [DecidableEq R] :
(normalize p).natDegree = p.natDegree
source
@[simp]
theorem Polynomial.natDegree_X_sub_C_sq_add_C_sq {R : Type u_1} [CommRing R] [NoZeroDivisors R] [Nontrivial R] (a b : R) :
((X - C a) ^ 2 + C b ^ 2).natDegree = 2
source
@[simp]
theorem Polynomial.monic_X_sub_C_sq_add_C_sq {R : Type u_1} [CommRing R] [NoZeroDivisors R] [Nontrivial R] (a b : R) :
((X - C a) ^ 2 + C b ^ 2).Monic
source
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
source
theorem Polynomial.has_root_of_odd_natDegree_imp_not_irreducible {F : Type u_1} [Field F] (h : ∀ (f : Polynomial F), Odd f.natDegree → f.natDegree ≠ 1 → ¬Irreducible f) {f : Polynomial F} (hf : Odd f.natDegree) :
∃ (x : F), f.IsRoot x
source
theorem Polynomial.has_root_of_monic_odd_natDegree_imp_not_irreducible {F : Type u_1} [Field F] (h : ∀ (f : Polynomial F), f.Monic → Odd f.natDegree → f.natDegree ≠ 1 → ¬Irreducible f) {f : Polynomial F} (hf : Odd f.natDegree) :
∃ (x : F), f.IsRoot x
source
theorem estimate {F : Type u_1} [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
source
theorem eventually_pos {F : Type u_1} [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
source
theorem estimate2 {F : Type u_1} [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' ⋯)
source
theorem eventually_neg {F : Type u_1} [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
source
theorem sign_change {F : Type u_1} [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
source
theorem Module.finrank_dvd_finrank (F : Type u_1) (K : Type u_2) (A : Type u_3) [Semiring F] [Ring K] [AddCommGroup A] [Module F K] [Module K A] [Module F A] [IsScalarTower F K A] [Nontrivial A] [StrongRankCondition F] [StrongRankCondition K] [Free F K] [Free K A] [Module.Finite K A] [NoZeroSMulDivisors K A] :
finrank F K = finrank F A / finrank K A
source
theorem Module.finrank_dvd_finrank' (F : Type u_1) (K : Type u_2) (A : Type u_3) [Ring F] [Ring K] [AddCommMonoid A] [Module F K] [Module K A] [Module F A] [IsScalarTower F K A] [Nontrivial K] [StrongRankCondition F] [StrongRankCondition K] [Free F K] [Free K A] [Module.Finite F K] [NoZeroSMulDivisors F K] :
finrank K A = finrank F A / finrank F K
source
theorem IsGalois.exists_intermediateField_of_pow_prime_dvd {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {p n : ℕ} (hp : Nat.Prime p) (hn : p ^ n ∣ Module.finrank K L) :
∃ (M : IntermediateField K L), Module.finrank (↥M) L = p ^ n
source
theorem IsGalois.exists_intermediateField_of_card_pow_prime_mul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {p n a : ℕ} (hp : Nat.Prime p) (hn : Module.finrank K L = p ^ n * a) {m : ℕ} (hm : m ≤ n) :
∃ (M : IntermediateField K L), Module.finrank K ↥M = p ^ m * a
source
theorem Sylow.exists_subgroup_le_card_pow_prime_of_card_pow_prime {G : Type u_1} [Group G] {m n p : ℕ} (hp : Nat.Prime p) {H : Subgroup G} (hH : Nat.card ↥H = p ^ n) (hm : m ≤ n) :
∃ H' ≤ H, Nat.card ↥H' = p ^ m
source
theorem IsGalois.exists_intermediateField_ge_card_pow_prime_of_card_pow_prime {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {m n p : ℕ} (hp : Nat.Prime p) {M : IntermediateField K L} (hM : Module.finrank (↥M) L = p ^ n) (hm : m ≤ n) :
∃ N ≥ M, Module.finrank (↥N) L = p ^ m
source
theorem IsGalois.exists_intermediateField_ge_card_pow_prime_mul_of_card_pow_prime_mul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {p n a : ℕ} (hp : Nat.Prime p) (hL : Module.finrank K L = p ^ n * a) {m m' : ℕ} {M : IntermediateField K L} (hM : Module.finrank K ↥M = p ^ m * a) (hm'₁ : m ≤ m') (hm'₂ : m' ≤ n) :
∃ N ≥ M, Module.finrank K ↥N = p ^ m' * a
source
theorem IsOrderedModule.of_algebraMap_mono {R : Type u_1} {A : Type u_2} [CommSemiring R] [Preorder R] [Semiring A] [PartialOrder A] [PosMulMono A] [MulPosMono A] [Algebra R A] (h : Monotone ⇑(algebraMap R A)) :
IsOrderedModule R A
source
theorem Module.nonempty_algEquiv_iff_finrank_eq_one {R : Type u_1} {S : Type u_2} [CommSemiring R] [StrongRankCondition R] [Semiring S] [Algebra R S] [Free R S] :
Nonempty (R ≃ₐ[R] S) ↔ finrank R S = 1
source
theorem IsAlgClosed.isSquare {k : Type u_1} [Field k] [IsAlgClosed k] (x : k) :
IsSquare x
source
theorem IsAlgClosed.of_finiteDimensional_imp_finrank_eq_one (k : Type u) [Field k] (H : ∀ (l : Type u) [inst : Field l] [inst_1 : Algebra k l] [FiniteDimensional k l], Module.finrank k l = 1) :
IsAlgClosed k