mathlib documentation

non_mathlib.cubic_alternate

theorem multiply_out_cubed (f : Type) [myfld f] (x a : f) :

cubed f x .+ a = (cubed f x) .+ ((three f) .* ((square f x) .* a) .+ ((three f) .* (x .* a .* a) .+ (cubed f a)))

def depressed_cubic_subst (f : Type) [myfld f] (c d x : f) :

f

Equations

depressed_cubic_subst f c d x = (cubed f x) .+ (c .* x .+ d)

theorem depressed_cubic_solution_two_vars (f : Type) [myfld f] (x c d s t : f) :

x = s .+ .- t ∧ c = (three f) .* (s .* t) ∧ d = (cubed f s) .+ .- (cubed f t) → (cubed f x) .+ c .* x = d

theorem depressed_cubic_simultaneous_solution (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 s t : f) (c_ne_zero : c ≠ myfld.zero) (s_ne_zero : s ≠ myfld.zero) :

s = fld_with_cube_root.cubrt (quadratic_formula f myfld.one .- d .- (cubed f c) .* (myfld.reciprocal (twenty_seven f) _) myfld.zero_distinct_one) → t = c .* (myfld.reciprocal (three f) .* s _) → c = (three f) .* (s .* t) ∧ d = (cubed f s) .+ .- (cubed f t)

theorem cardano_den_ne_zero (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 : f) (c_ne_zero : c ≠ myfld.zero) :

quadratic_formula f myfld.one d .- (cubed f c) .* (myfld.reciprocal (twenty_seven f) _) myfld.zero_distinct_one ≠ myfld.zero

def cardano_formula_new (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 : f) (c_ne_zero : c ≠ myfld.zero) (cubrt_func : f → f) (cubrt_func_nonzero : ∀ (x : f), x ≠ myfld.zero → cubrt_func x ≠ myfld.zero) (cubrt_func_correct : ∀ (x : f), cubed f (cubrt_func x) = x) :

f

Equations

cardano_formula_new f c d c_ne_zero cubrt_func cubrt_func_nonzero cubrt_func_correct = (fld_with_cube_root.cubrt (quadratic_formula f myfld.one d .- (cubed f c) .* (myfld.reciprocal (twenty_seven f) _) myfld.zero_distinct_one)) .+ .- (c .* (myfld.reciprocal (three f) .* (fld_with_cube_root.cubrt (quadratic_formula f myfld.one d .- (cubed f c) .* (myfld.reciprocal (twenty_seven f) _) myfld.zero_distinct_one)) _))

def cardano_formula_a_new (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 : f) (c_ne_zero : c ≠ myfld.zero) :

f

Equations

cardano_formula_a_new f c d c_ne_zero = cardano_formula_new f c d c_ne_zero fld_with_cube_root.cubrt _ _

def cardano_formula_b_new (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 : f) (c_ne_zero : c ≠ myfld.zero) :

f

Equations

cardano_formula_b_new f c d c_ne_zero = cardano_formula_new f c d c_ne_zero (alt_cubrt_a f) _ _

def cardano_formula_c_new (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 : f) (c_ne_zero : c ≠ myfld.zero) :

f

Equations

cardano_formula_c_new f c d c_ne_zero = cardano_formula_new f c d c_ne_zero (alt_cubrt_b f) _ _

theorem cardano_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 : f) (c_ne_zero : c ≠ myfld.zero) (cubrt_func : f → f) (cubrt_func_nonzero : ∀ (x : f), x ≠ myfld.zero → cubrt_func x ≠ myfld.zero) (cubrt_func_correct : ∀ (x : f), cubed f (cubrt_func x) = x) :

depressed_cubic_subst f c d (cardano_formula_new f c d c_ne_zero cubrt_func cubrt_func_nonzero cubrt_func_correct) = myfld.zero

def cubic_subst (f : Type) [myfld f] (a b c d x : f) :

f

Equations

cubic_subst f a b c d x = a .* (cubed f x) .+ (b .* (square f x) .+ (c .* x .+ d))

theorem divide_cubic_through (f : Type) [myfld f] (a b c d x : f) (a_ne_zero : a ≠ myfld.zero) :

cubic_subst f a b c d x = myfld.zero ↔ cubic_subst f myfld.one b .* (myfld.reciprocal a a_ne_zero) c .* (myfld.reciprocal a a_ne_zero) d .* (myfld.reciprocal a a_ne_zero) x = myfld.zero

def third (f : Type) [myfld f] [fld_not_char_three f] :

f

Equations

third f = myfld.reciprocal (three f) fld_not_char_three.not_char_three

def twenty_seventh (f : Type) [myfld f] [fld_not_char_three f] :

f

Equations

twenty_seventh f = myfld.reciprocal (twenty_seven f) _

theorem depressed_cubic_equal_split (f : Type) [myfld f] (c1 d1 c2 d2 x : f) :

c1 = c2 ∧ d1 = d2 → depressed_cubic_subst f c1 d1 x = depressed_cubic_subst f c2 d2 x

theorem helper_bcubed (f : Type) [myfld f] [fld_not_char_three f] (b : f) :

b .* ((third f) .* (b .* ((third f) .* b))) = (three f) .* ((myfld.reciprocal (twenty_seven f) _) .* (b .* b .* b))

theorem helper_twothirds (f : Type) [myfld f] [fld_not_char_three f] :

.- (third f) .+ myfld.one = (third f) .+ (third f)

theorem reduce_cubic_to_depressed (f : Type) [myfld f] [fld_not_char_three f] (b c d x y : f) :

x = y .+ .- (b .* (third f)) → cubic_subst f myfld.one b c d x = depressed_cubic_subst f (square f b) .* .- (third f) .+ c (twenty_seventh f) .* ((two f) .* (cubed f b) .+ .- ((nine f) .* (b .* c)) .+ (twenty_seven f) .* d) y

theorem int_quantity_ne_zero_simp (f : Type) [myfld f] [fld_not_char_three f] (a1 b c : f) (a_ne_zero : a1 ≠ myfld.zero) :

(three f) .* (a1 .* c) .+ .- (square f b) ≠ myfld.zero → (square f b .* (myfld.reciprocal a1 a_ne_zero)) .* .- (third f) .+ c .* (myfld.reciprocal a1 a_ne_zero) ≠ myfld.zero

def cubic_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 : f) (a_ne_zero : a ≠ myfld.zero) (int_quantity_ne_zero : (three f) .* (a .* c) .+ .- (square f b) ≠ myfld.zero) :

f

Equations

cubic_formula_a f a b c d a_ne_zero int_quantity_ne_zero = (cardano_formula_a_new f (square f b .* (myfld.reciprocal a a_ne_zero)) .* .- (third f) .+ c .* (myfld.reciprocal a a_ne_zero) (twenty_seventh f) .* ((two f) .* (cubed f b .* (myfld.reciprocal a a_ne_zero)) .+ .- ((nine f) .* (b .* (myfld.reciprocal a a_ne_zero) .* (c .* (myfld.reciprocal a a_ne_zero)))) .+ (twenty_seven f) .* (d .* (myfld.reciprocal a a_ne_zero))) _) .+ .- (b .* (myfld.reciprocal a a_ne_zero) .* (third f))

theorem cubic_formula_a_correct (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 : f) (a_ne_zero : a ≠ myfld.zero) (int_quantity_ne_zero : (three f) .* (a .* c) .+ .- (square f b) ≠ myfld.zero) :

cubic_subst f a b c d (cubic_formula_a f a b c d a_ne_zero int_quantity_ne_zero) = myfld.zero