mathlib documentation

non-mathlib.quartic

source
theorem not_char_four (f : Type) [myfld f] [fld_not_char_two f] :
four f ≠ myfld.zero
source
def fourth_power (f : Type) [myfld f] (a : f) :
f
Equations
source
theorem fourth_power_of_product (f : Type) [myfld f] (a b : f) :
fourth_power f a .* b = (fourth_power f a) .* (fourth_power f b)
source
theorem fourth_power_negate (f : Type) [myfld f] (a : f) :
fourth_power f .- a = fourth_power f a
source
def fourth_root_a (f : Type) [myfld f] [fld_with_sqrt f] (a : f) :
f
Equations
source
theorem fourth_root_to_power_a (f : Type) [myfld f] [fld_with_sqrt f] (a : f) :
fourth_power f (fourth_root_a f a) = a
source
def fourth_root_b (f : Type) [myfld f] [fld_with_sqrt f] (a : f) :
f
Equations
source
theorem fourth_root_to_power_b (f : Type) [myfld f] [fld_with_sqrt f] (a : f) :
fourth_power f (fourth_root_b f a) = a
source
def fourth_root_c (f : Type) [myfld f] [fld_with_sqrt f] (a : f) :
f
Equations
source
theorem fourth_root_to_power_c (f : Type) [myfld f] [fld_with_sqrt f] (a : f) :
fourth_power f (fourth_root_c f a) = a
source
def fourth_root_d (f : Type) [myfld f] [fld_with_sqrt f] (a : f) :
f
Equations
source
theorem fourth_root_to_power_d (f : Type) [myfld f] [fld_with_sqrt f] (a : f) :
fourth_power f (fourth_root_d f a) = a
source
def factorized_quartic_expression (f : Type) [myfld f] (x a1 a2 a3 a4 : f) :
f
Equations
source
def quartic_expression (f : Type) [myfld f] (x a b c d e : f) :
f
Equations
source
theorem multiply_out_quartic (f : Type) [myfld f] (x a1 a2 a3 a4 : f) :
factorized_quartic_expression f x a1 a2 a3 a4 = quartic_expression f x myfld.one .- (a1 .+ (a2 .+ (a3 .+ a4))) a1 .* a2 .+ (a1 .* a3 .+ (a1 .* a4 .+ (a2 .* a3 .+ (a2 .* a4 .+ a3 .* a4)))) .- (a1 .* (a2 .* a3) .+ (a1 .* (a2 .* a4) .+ (a1 .* (a3 .* a4) .+ a2 .* (a3 .* a4)))) a1 .* (a2 .* (a3 .* a4))
source
theorem multiply_out_fourth_power (f : Type) [myfld f] (x y : f) :
fourth_power f x .+ y = quartic_expression f x myfld.one (four f) .* y (six f) .* (square f y) (four f) .* (cubed f y) (fourth_power f y)
source
theorem sum_of_fourth_roots (f : Type) [myfld f] [fld_with_sqrt f] (x : f) :
(fourth_root_a f x) .+ ((fourth_root_b f x) .+ ((fourth_root_c f x) .+ (fourth_root_d f x))) = myfld.zero
source
theorem no_other_fourth_roots (f : Type) [myfld f] [fld_with_sqrt f] (x root : f) :
root ≠ fourth_root_a f x → root ≠ fourth_root_b f x → root ≠ fourth_root_c f x → root ≠ fourth_root_d f x → fourth_power f root ≠ x
source
theorem remove_fourth_power_coefficient (f : Type) [myfld f] (a b c d e x : f) (a_ne_zero : a ≠ myfld.zero) :
quartic_expression f x a b c d e = myfld.zero ↔ quartic_expression f x myfld.one b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero) e .* (myfld.reciprocal a a_ne_zero) = myfld.zero
source
def depressed_quartic_subst (f : Type) [myfld f] (c d e x : f) :
f
Equations
source
def pow_of_two (f : Type) [myfld f] :
ℕ → f
Equations
source
theorem pow_of_two_nonzero (f : Type) [myfld f] [fld_not_char_two f] (exp : ℕ) :
pow_of_two f exp ≠ myfld.zero
source
def depressed_quartic_squ_coeff (f : Type) [myfld f] [fld_not_char_two f] (b c : f) :
f
Equations
source
def depressed_quartic_linear_coeff (f : Type) [myfld f] [fld_not_char_two f] (b c d : f) :
f
Equations
source
def depressed_quartic_constant (f : Type) [myfld f] [fld_not_char_two f] (b c d e : f) :
f
Equations
source
theorem quartic_reduce_x_squ_helper (f : Type) [myfld f] [fld_not_char_two f] (b c : f) :
.- ((three f) .* (b .* ((myfld.reciprocal (four f) _) .* b))) .+ (c .+ (six f) .* ((myfld.reciprocal (square f (four f)) _) .* (square f b))) = depressed_quartic_squ_coeff f b c
source
theorem quartic_reduce_linear_helper (f : Type) [myfld f] [fld_not_char_two f] (b c d : f) :
.- ((two f) .* (b .* ((myfld.reciprocal (four f) _) .* c))) .+ d .+ .- ((four f) .* (cubed f (myfld.reciprocal (four f) _) .* b)) .+ (three f) .* (b .* ((myfld.reciprocal (four f) _) .* (b .* ((myfld.reciprocal (four f) _) .* b)))) = depressed_quartic_linear_coeff f b c d
source
theorem quartic_reduce_constant_helper (f : Type) [myfld f] [fld_not_char_two f] (b c d e : f) :
(fourth_power f .- ((myfld.reciprocal (four f) _) .* b)) .+ ( .- ((cubed f (myfld.reciprocal (four f) _) .* b) .* b) .+ ((myfld.reciprocal (square f (four f)) _) .* ((square f b) .* c) .+ ( .- (b .* ((myfld.reciprocal (four f) _) .* d)) .+ e))) = depressed_quartic_constant f b c d e
source
theorem reduce_quartic_to_depressed (f : Type) [myfld f] [fld_not_char_two f] (b c d e x u : f) :
x = u .+ .- (b .* (myfld.reciprocal (four f) _)) → quartic_expression f x myfld.one b c d e = depressed_quartic_subst f (depressed_quartic_squ_coeff f b c) (depressed_quartic_linear_coeff f b c d) (depressed_quartic_constant f b c d e) u
source
theorem depressed_quartic_to_quadratic_product (f : Type) [myfld f] (c d e p q s x : f) (p_ne_zero : p ≠ myfld.zero) :
c .+ (square f p) = s .+ q ∧ d .* (myfld.reciprocal p p_ne_zero) = s .+ .- q ∧ e = s .* q → depressed_quartic_subst f c d e x = (quadratic_subst f x myfld.one p q) .* (quadratic_subst f x myfld.one .- p s)
source
theorem simultaneous_solution_helper (f : Type) [myfld f] [fld_not_char_two f] (c d e p q s : f) (p_ne_zero : p ≠ myfld.zero) :
cubic_subst f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) (square f p) = myfld.zero → e = (myfld.reciprocal (two f) .* (two f) _) .* ((fourth_power f p) .+ ((two f) .* (c .* (square f p)) .+ (square f c))) .+ (myfld.reciprocal (two f) .* (two f) _) .* .- (square f d .* (myfld.reciprocal p p_ne_zero))
source
theorem simultaneous_solution (f : Type) [_inst_1 _inst_2 : myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (c d e p q s : f) (p_ne_zero : p ≠ myfld.zero) (int_quantity_ne_zero : (three f) .* (myfld.one .* ((square f c) .+ .- ((four f) .* e))) .+ .- (square f (two f) .* c) ≠ myfld.zero) :
p = sqroot (cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero) → s = (myfld.reciprocal (two f) fld_not_char_two.not_char_two) .* (c .+ ((square f p) .+ d .* (myfld.reciprocal p p_ne_zero))) → q = (myfld.reciprocal (two f) fld_not_char_two.not_char_two) .* (c .+ ((square f p) .+ .- d .* (myfld.reciprocal p p_ne_zero))) → c .+ (square f p) = s .+ q ∧ d .* (myfld.reciprocal p p_ne_zero) = s .+ .- q ∧ e = s .* q
source
theorem depressed_quartic_to_quadratic_product_solved (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (c d e x : f) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f c) .+ .- ((four f) .* e))) .+ .- (square f (two f) .* c) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
depressed_quartic_subst f c d e x = (quadratic_subst f x myfld.one sqroot (cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a) (myfld.reciprocal (two f) fld_not_char_two.not_char_two) .* (c .+ ((square f sqroot (cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a)) .+ .- d .* (myfld.reciprocal sqroot (cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a) _)))) .* (quadratic_subst f x myfld.one .- sqroot (cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a) (myfld.reciprocal (two f) fld_not_char_two.not_char_two) .* (c .+ ((square f sqroot (cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a)) .+ d .* (myfld.reciprocal sqroot (cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a) _))))
source
theorem depressed_quartic_to_linear_factorization (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (c d e x : f) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f c) .+ .- ((four f) .* e))) .+ .- (square f (two f) .* c) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
depressed_quartic_subst f c d e x = (x .+ .- (quadratic_formula f myfld.one sqroot (cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a) (myfld.reciprocal (two f) fld_not_char_two.not_char_two) .* (c .+ ((square f sqroot (cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a)) .+ .- d .* (myfld.reciprocal sqroot (cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a) _))) myfld.zero_distinct_one)) .* (x .+ .- (quadratic_formula_alt f myfld.one sqroot (cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a) (myfld.reciprocal (two f) fld_not_char_two.not_char_two) .* (c .+ ((square f sqroot (cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a)) .+ .- d .* (myfld.reciprocal sqroot (cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a) _))) myfld.zero_distinct_one)) .* (x .+ .- (quadratic_formula f myfld.one .- sqroot (cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a) (myfld.reciprocal (two f) fld_not_char_two.not_char_two) .* (c .+ ((square f sqroot (cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a)) .+ d .* (myfld.reciprocal sqroot (cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a) _))) myfld.zero_distinct_one)) .* (x .+ .- (quadratic_formula_alt f myfld.one .- sqroot (cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a) (myfld.reciprocal (two f) fld_not_char_two.not_char_two) .* (c .+ ((square f sqroot (cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a)) .+ d .* (myfld.reciprocal sqroot (cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a) _))) myfld.zero_distinct_one))
source
theorem quadratic_product_solution (f : Type) [myfld f] [fld_not_char_two f] [fld_with_sqrt f] (b1 b2 c1 c2 x : f) :
x = quadratic_formula f myfld.one b1 c1 myfld.zero_distinct_one ∨ x = quadratic_formula_alt f myfld.one b1 c1 myfld.zero_distinct_one ∨ x = quadratic_formula f myfld.one b2 c2 myfld.zero_distinct_one ∨ x = quadratic_formula_alt f myfld.one b2 c2 myfld.zero_distinct_one → (quadratic_subst f x myfld.one b1 c1) .* (quadratic_subst f x myfld.one b2 c2) = myfld.zero
source
theorem quadratic_product_solution_unique (f : Type) [myfld f] [fld_not_char_two f] [fld_with_sqrt f] (b1 b2 c1 c2 x : f) :
x ≠ quadratic_formula f myfld.one b1 c1 myfld.zero_distinct_one → x ≠ quadratic_formula_alt f myfld.one b1 c1 myfld.zero_distinct_one → x ≠ quadratic_formula f myfld.one b2 c2 myfld.zero_distinct_one → x ≠ quadratic_formula_alt f myfld.one b2 c2 myfld.zero_distinct_one → (quadratic_subst f x myfld.one b1 c1) .* (quadratic_subst f x myfld.one b2 c2) ≠ myfld.zero
source
def depressed_quartic_solution_a (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (c d e : f) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f c) .+ .- ((four f) .* e))) .+ .- (square f (two f) .* c) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
f
Equations
source
theorem depressed_quartic_solution_a_works (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (c d e : f) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f c) .+ .- ((four f) .* e))) .+ .- (square f (two f) .* c) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
depressed_quartic_subst f c d e (depressed_quartic_solution_a f c d e int_quantity_ne_zero_a int_quantity_ne_zero_b) = myfld.zero
source
def depressed_quartic_solution_b (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (c d e : f) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f c) .+ .- ((four f) .* e))) .+ .- (square f (two f) .* c) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
f
Equations
source
theorem depressed_quartic_solution_b_works (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (c d e : f) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f c) .+ .- ((four f) .* e))) .+ .- (square f (two f) .* c) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
depressed_quartic_subst f c d e (depressed_quartic_solution_b f c d e int_quantity_ne_zero_a int_quantity_ne_zero_b) = myfld.zero
source
def depressed_quartic_solution_c (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (c d e : f) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f c) .+ .- ((four f) .* e))) .+ .- (square f (two f) .* c) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
f
Equations
source
theorem depressed_quartic_solution_c_works (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (c d e : f) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f c) .+ .- ((four f) .* e))) .+ .- (square f (two f) .* c) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
depressed_quartic_subst f c d e (depressed_quartic_solution_c f c d e int_quantity_ne_zero_a int_quantity_ne_zero_b) = myfld.zero
source
def depressed_quartic_solution_d (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (c d e : f) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f c) .+ .- ((four f) .* e))) .+ .- (square f (two f) .* c) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
f
Equations
source
theorem depressed_quartic_solution_d_works (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (c d e : f) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f c) .+ .- ((four f) .* e))) .+ .- (square f (two f) .* c) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
depressed_quartic_subst f c d e (depressed_quartic_solution_d f c d e int_quantity_ne_zero_a int_quantity_ne_zero_b) = myfld.zero
source
theorem depressed_quartic_solution_uniqueness (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (c d e x : f) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f c) .+ .- ((four f) .* e))) .+ .- (square f (two f) .* c) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* c (square f c) .+ .- ((four f) .* e) .- (square f d) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
x ≠ depressed_quartic_solution_a f c d e int_quantity_ne_zero_a int_quantity_ne_zero_b → x ≠ depressed_quartic_solution_b f c d e int_quantity_ne_zero_a int_quantity_ne_zero_b → x ≠ depressed_quartic_solution_c f c d e int_quantity_ne_zero_a int_quantity_ne_zero_b → x ≠ depressed_quartic_solution_d f c d e int_quantity_ne_zero_a int_quantity_ne_zero_b → depressed_quartic_subst f c d e x ≠ myfld.zero
source
def quartic_formula_int_a (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (b c d e : f) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f (depressed_quartic_squ_coeff f b c)) .+ .- ((four f) .* (depressed_quartic_constant f b c d e)))) .+ .- (square f (two f) .* (depressed_quartic_squ_coeff f b c)) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* (depressed_quartic_squ_coeff f b c) (square f (depressed_quartic_squ_coeff f b c)) .+ .- ((four f) .* (depressed_quartic_constant f b c d e)) .- (square f (depressed_quartic_linear_coeff f b c d)) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
f
Equations
source
theorem quartic_formula_int_a_works (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (b c d e : f) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f (depressed_quartic_squ_coeff f b c)) .+ .- ((four f) .* (depressed_quartic_constant f b c d e)))) .+ .- (square f (two f) .* (depressed_quartic_squ_coeff f b c)) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* (depressed_quartic_squ_coeff f b c) (square f (depressed_quartic_squ_coeff f b c)) .+ .- ((four f) .* (depressed_quartic_constant f b c d e)) .- (square f (depressed_quartic_linear_coeff f b c d)) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
quartic_expression f (quartic_formula_int_a f b c d e int_quantity_ne_zero_a int_quantity_ne_zero_b) myfld.one b c d e = myfld.zero
source
def quartic_formula_a (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (a b c d e : f) (a_ne_zero : a ≠ myfld.zero) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) .+ .- ((four f) .* (depressed_quartic_constant f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero) e .* (myfld.reciprocal a a_ne_zero))))) .+ .- (square f (two f) .* (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero)) (square f (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) .+ .- ((four f) .* (depressed_quartic_constant f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero) e .* (myfld.reciprocal a a_ne_zero))) .- (square f (depressed_quartic_linear_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero))) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
f
Equations
source
theorem quartic_formula_a_works (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (a b c d e : f) (a_ne_zero : a ≠ myfld.zero) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) .+ .- ((four f) .* (depressed_quartic_constant f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero) e .* (myfld.reciprocal a a_ne_zero))))) .+ .- (square f (two f) .* (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero)) (square f (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) .+ .- ((four f) .* (depressed_quartic_constant f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero) e .* (myfld.reciprocal a a_ne_zero))) .- (square f (depressed_quartic_linear_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero))) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
quartic_expression f (quartic_formula_a f a b c d e a_ne_zero int_quantity_ne_zero_a int_quantity_ne_zero_b) a b c d e = myfld.zero
source
def quartic_formula_int_b (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (b c d e : f) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f (depressed_quartic_squ_coeff f b c)) .+ .- ((four f) .* (depressed_quartic_constant f b c d e)))) .+ .- (square f (two f) .* (depressed_quartic_squ_coeff f b c)) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* (depressed_quartic_squ_coeff f b c) (square f (depressed_quartic_squ_coeff f b c)) .+ .- ((four f) .* (depressed_quartic_constant f b c d e)) .- (square f (depressed_quartic_linear_coeff f b c d)) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
f
Equations
source
theorem quartic_formula_int_b_works (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (b c d e : f) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f (depressed_quartic_squ_coeff f b c)) .+ .- ((four f) .* (depressed_quartic_constant f b c d e)))) .+ .- (square f (two f) .* (depressed_quartic_squ_coeff f b c)) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* (depressed_quartic_squ_coeff f b c) (square f (depressed_quartic_squ_coeff f b c)) .+ .- ((four f) .* (depressed_quartic_constant f b c d e)) .- (square f (depressed_quartic_linear_coeff f b c d)) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
quartic_expression f (quartic_formula_int_b f b c d e int_quantity_ne_zero_a int_quantity_ne_zero_b) myfld.one b c d e = myfld.zero
source
def quartic_formula_b (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (a b c d e : f) (a_ne_zero : a ≠ myfld.zero) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) .+ .- ((four f) .* (depressed_quartic_constant f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero) e .* (myfld.reciprocal a a_ne_zero))))) .+ .- (square f (two f) .* (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero)) (square f (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) .+ .- ((four f) .* (depressed_quartic_constant f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero) e .* (myfld.reciprocal a a_ne_zero))) .- (square f (depressed_quartic_linear_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero))) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
f
Equations
source
theorem quartic_formula_b_works (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (a b c d e : f) (a_ne_zero : a ≠ myfld.zero) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) .+ .- ((four f) .* (depressed_quartic_constant f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero) e .* (myfld.reciprocal a a_ne_zero))))) .+ .- (square f (two f) .* (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero)) (square f (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) .+ .- ((four f) .* (depressed_quartic_constant f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero) e .* (myfld.reciprocal a a_ne_zero))) .- (square f (depressed_quartic_linear_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero))) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
quartic_expression f (quartic_formula_b f a b c d e a_ne_zero int_quantity_ne_zero_a int_quantity_ne_zero_b) a b c d e = myfld.zero
source
def quartic_formula_int_c (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (b c d e : f) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f (depressed_quartic_squ_coeff f b c)) .+ .- ((four f) .* (depressed_quartic_constant f b c d e)))) .+ .- (square f (two f) .* (depressed_quartic_squ_coeff f b c)) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* (depressed_quartic_squ_coeff f b c) (square f (depressed_quartic_squ_coeff f b c)) .+ .- ((four f) .* (depressed_quartic_constant f b c d e)) .- (square f (depressed_quartic_linear_coeff f b c d)) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
f
Equations
source
theorem quartic_formula_int_c_works (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (b c d e : f) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f (depressed_quartic_squ_coeff f b c)) .+ .- ((four f) .* (depressed_quartic_constant f b c d e)))) .+ .- (square f (two f) .* (depressed_quartic_squ_coeff f b c)) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* (depressed_quartic_squ_coeff f b c) (square f (depressed_quartic_squ_coeff f b c)) .+ .- ((four f) .* (depressed_quartic_constant f b c d e)) .- (square f (depressed_quartic_linear_coeff f b c d)) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
quartic_expression f (quartic_formula_int_c f b c d e int_quantity_ne_zero_a int_quantity_ne_zero_b) myfld.one b c d e = myfld.zero
source
def quartic_formula_c (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (a b c d e : f) (a_ne_zero : a ≠ myfld.zero) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) .+ .- ((four f) .* (depressed_quartic_constant f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero) e .* (myfld.reciprocal a a_ne_zero))))) .+ .- (square f (two f) .* (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero)) (square f (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) .+ .- ((four f) .* (depressed_quartic_constant f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero) e .* (myfld.reciprocal a a_ne_zero))) .- (square f (depressed_quartic_linear_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero))) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
f
Equations
source
theorem quartic_formula_c_works (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (a b c d e : f) (a_ne_zero : a ≠ myfld.zero) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) .+ .- ((four f) .* (depressed_quartic_constant f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero) e .* (myfld.reciprocal a a_ne_zero))))) .+ .- (square f (two f) .* (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero)) (square f (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) .+ .- ((four f) .* (depressed_quartic_constant f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero) e .* (myfld.reciprocal a a_ne_zero))) .- (square f (depressed_quartic_linear_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero))) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
quartic_expression f (quartic_formula_c f a b c d e a_ne_zero int_quantity_ne_zero_a int_quantity_ne_zero_b) a b c d e = myfld.zero
source
def quartic_formula_int_d (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (b c d e : f) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f (depressed_quartic_squ_coeff f b c)) .+ .- ((four f) .* (depressed_quartic_constant f b c d e)))) .+ .- (square f (two f) .* (depressed_quartic_squ_coeff f b c)) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* (depressed_quartic_squ_coeff f b c) (square f (depressed_quartic_squ_coeff f b c)) .+ .- ((four f) .* (depressed_quartic_constant f b c d e)) .- (square f (depressed_quartic_linear_coeff f b c d)) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
f
Equations
source
theorem quartic_formula_int_d_works (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (b c d e : f) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f (depressed_quartic_squ_coeff f b c)) .+ .- ((four f) .* (depressed_quartic_constant f b c d e)))) .+ .- (square f (two f) .* (depressed_quartic_squ_coeff f b c)) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* (depressed_quartic_squ_coeff f b c) (square f (depressed_quartic_squ_coeff f b c)) .+ .- ((four f) .* (depressed_quartic_constant f b c d e)) .- (square f (depressed_quartic_linear_coeff f b c d)) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
quartic_expression f (quartic_formula_int_d f b c d e int_quantity_ne_zero_a int_quantity_ne_zero_b) myfld.one b c d e = myfld.zero
source
def quartic_formula_d (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (a b c d e : f) (a_ne_zero : a ≠ myfld.zero) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) .+ .- ((four f) .* (depressed_quartic_constant f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero) e .* (myfld.reciprocal a a_ne_zero))))) .+ .- (square f (two f) .* (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero)) (square f (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) .+ .- ((four f) .* (depressed_quartic_constant f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero) e .* (myfld.reciprocal a a_ne_zero))) .- (square f (depressed_quartic_linear_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero))) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
f
Equations
source
theorem quartic_formula_d_works (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (a b c d e : f) (a_ne_zero : a ≠ myfld.zero) (int_quantity_ne_zero_a : (three f) .* (myfld.one .* ((square f (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) .+ .- ((four f) .* (depressed_quartic_constant f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero) e .* (myfld.reciprocal a a_ne_zero))))) .+ .- (square f (two f) .* (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) ≠ myfld.zero) (int_quantity_ne_zero_b : cubic_formula_a f myfld.one (two f) .* (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero)) (square f (depressed_quartic_squ_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero))) .+ .- ((four f) .* (depressed_quartic_constant f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero) e .* (myfld.reciprocal a a_ne_zero))) .- (square f (depressed_quartic_linear_coeff f b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero))) myfld.zero_distinct_one int_quantity_ne_zero_a ≠ myfld.zero) :
quartic_expression f (quartic_formula_d f a b c d e a_ne_zero int_quantity_ne_zero_a int_quantity_ne_zero_b) a b c d e = myfld.zero