non-mathlib.cubic - mathlib docs

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 cardano_intermediate_val (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] [fld_not_char_three f] (c d : f) :

f

Equations

cardano_intermediate_val f c d = sqroot ((square f d) .* (myfld.reciprocal (four f) _) .+ (cubed f c) .* (myfld.reciprocal (twenty_seven f) _))

source

def cardano_other_int_val (f : Type) [myfld f] [fld_not_char_two f] (d : f) :

f

Equations

cardano_other_int_val f d = .- (d .* (myfld.reciprocal (two f) fld_not_char_two.not_char_two))

source

theorem cardano_den_not_zero_general (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] [fld_not_char_three f] (c d : f) (c_ne_zero : c ≠ myfld.zero) :

(square f (cardano_intermediate_val f c d)) .+ .- (square f (cardano_other_int_val f d)) ≠ myfld.zero

source

theorem cardano_den_not_zero_int (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] [fld_not_char_three f] (c d : f) (c_ne_zero : c ≠ myfld.zero) :

(cardano_intermediate_val f c d) .+ (cardano_other_int_val f d) ≠ myfld.zero

source

theorem cardano_den_not_zero_int_alt (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] [fld_not_char_three f] (c d : f) (c_ne_zero : c ≠ myfld.zero) :

(cardano_intermediate_val f c d) .+ .- (cardano_other_int_val f d) ≠ myfld.zero

source

theorem cardano_denominator_not_zero (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] [fld_not_char_three f] [fld_with_cube_root 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 (cardano_intermediate_val f c d) .+ (cardano_other_int_val f d)) .* (three f) ≠ myfld.zero

source

def cardano_formula (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 f c d c_ne_zero cubrt_func cubrt_func_nonzero cubrt_func_correct = (cubrt_func (cardano_intermediate_val f c d) .+ (cardano_other_int_val f d)) .+ .- (c .* (myfld.reciprocal (cubrt_func (cardano_intermediate_val f c d) .+ (cardano_other_int_val f d)) .* (three f) _))

source

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)

source

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 f c d c_ne_zero cubrt_func cubrt_func_nonzero cubrt_func_correct) = myfld.zero

source

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

f

Equations

cardano_formula_a f c d c_ne_zero = cardano_formula f c d c_ne_zero fld_with_cube_root.cubrt _ _

source

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

f

Equations

cardano_formula_b f c d c_ne_zero = cardano_formula f c d c_ne_zero (alt_cubrt_a f) _ _

source

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

f

Equations

cardano_formula_c f c d c_ne_zero = cardano_formula f c d c_ne_zero (alt_cubrt_b f) _ _

source

def depressed_cubic_solution_c_zero (f : Type) [myfld f] (c d : f) (c_eq_zero : c = myfld.zero) (cubrt_func : f → f) (cubrt_func_correct : ∀ (x : f), cubed f (cubrt_func x) = x) :

f

Equations

depressed_cubic_solution_c_zero f c d c_eq_zero cubrt_func cubrt_func_correct = .- (cubrt_func d)

source

theorem depressed_cubic_solution_c_zero_correct (f : Type) [myfld f] (c d : f) (c_eq_zero : c = myfld.zero) (cubrt_func : f → f) (cubrt_func_correct : ∀ (x : f), cubed f (cubrt_func x) = x) :

depressed_cubic_subst f c d (depressed_cubic_solution_c_zero f c d c_eq_zero cubrt_func cubrt_func_correct) = myfld.zero

source

def depressed_cubic_solution_c_zero_a (f : Type) [myfld f] [fld_with_cube_root f] (c d : f) (c_eq_zero : c = myfld.zero) :

f

Equations

depressed_cubic_solution_c_zero_a f c d c_eq_zero = depressed_cubic_solution_c_zero f c d c_eq_zero fld_with_cube_root.cubrt _

source

def depressed_cubic_solution_c_zero_b (f : Type) [myfld f] [fld_with_cube_root f] [fld_with_sqrt f] [fld_not_char_two f] (c d : f) (c_eq_zero : c = myfld.zero) :

f

Equations

depressed_cubic_solution_c_zero_b f c d c_eq_zero = depressed_cubic_solution_c_zero f c d c_eq_zero (alt_cubrt_a f) _

source

def depressed_cubic_solution_c_zero_c (f : Type) [myfld f] [fld_with_cube_root f] [fld_with_sqrt f] [fld_not_char_two f] (c d : f) (c_eq_zero : c = myfld.zero) :

f

Equations

depressed_cubic_solution_c_zero_c f c d c_eq_zero = depressed_cubic_solution_c_zero f c d c_eq_zero (alt_cubrt_b f) _

source

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))

source

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

source

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

source

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

f

Equations

twenty_seventh f = myfld.reciprocal (twenty_seven f) _

source

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

source

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))

source

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

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

source

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

source

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

source

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 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))

source

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

source

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

f

Equations

cubic_formula_b f a b c d a_ne_zero int_quantity_ne_zero = (cardano_formula_b 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))

source

theorem cubic_formula_b_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_b f a b c d a_ne_zero int_quantity_ne_zero) = myfld.zero

source

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

f

Equations

cubic_formula_c f a b c d a_ne_zero int_quantity_ne_zero = (cardano_formula_c 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))

source

theorem cubic_formula_c_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_c f a b c d a_ne_zero int_quantity_ne_zero) = myfld.zero

source

theorem int_quantity_eq_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

source

def cubic_formula_a_alt (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_eq_zero : (three f) .* (a .* c) .+ .- (square f b) = myfld.zero) :

f

Equations

cubic_formula_a_alt f a b c d a_ne_zero int_quantity_eq_zero = (depressed_cubic_solution_c_zero_a 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))

source

theorem cubic_formula_a_alt_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_eq_zero : (three f) .* (a .* c) .+ .- (square f b) = myfld.zero) :

cubic_subst f a b c d (cubic_formula_a_alt f a b c d a_ne_zero int_quantity_eq_zero) = myfld.zero

source

def cubic_formula_b_alt (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_eq_zero : (three f) .* (a .* c) .+ .- (square f b) = myfld.zero) :

f

Equations

cubic_formula_b_alt f a b c d a_ne_zero int_quantity_eq_zero = (depressed_cubic_solution_c_zero_b 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))

source

def cubic_formula_c_alt (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_eq_zero : (three f) .* (a .* c) .+ .- (square f b) = myfld.zero) :

f

Equations

cubic_formula_c_alt f a b c d a_ne_zero int_quantity_eq_zero = (depressed_cubic_solution_c_zero_c 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))

source

theorem cube_roots_sum_zero (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] [fld_with_cube_root f] (x : f) :

(fld_with_cube_root.cubrt x) .+ ((alt_cubrt_a f x) .+ (alt_cubrt_b f x)) = myfld.zero

source

theorem cardano_formulae_sum_zero (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] [fld_with_cube_root f] [fld_not_char_three f] (c d : f) (c_ne_zero : c ≠ myfld.zero) :

(cardano_formula_a f c d c_ne_zero) .+ ((cardano_formula_b f c d c_ne_zero) .+ (cardano_formula_c f c d c_ne_zero)) = myfld.zero

source

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

(cardano_formula_a f c d c_ne_zero) .* (cardano_formula_b f c d c_ne_zero) .+ (cardano_formula_a f c d c_ne_zero) .* (cardano_formula_c f c d c_ne_zero) .+ (cardano_formula_b f c d c_ne_zero) .* (cardano_formula_c f c d c_ne_zero) = c

source

theorem cardano_product_helper (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) :

(cardano_intermediate_val f c d) .+ (cardano_other_int_val f d) .+ .- ((myfld.reciprocal (cardano_intermediate_val f c d) .+ (cardano_other_int_val f d) _) .* (myfld.reciprocal (three f) .* ((three f) .* (three f)) _) .* (c .* c) .* c) = .- d

source

theorem cardano_product (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) :

(cardano_formula_a f c d c_ne_zero) .* ((cardano_formula_b f c d c_ne_zero) .* (cardano_formula_c f c d c_ne_zero)) = .- d

source

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

depressed_cubic_subst f c d x = factorized_cubic_expression f x (cardano_formula_a f c d c_ne_zero) (cardano_formula_b f c d c_ne_zero) (cardano_formula_c f c d c_ne_zero)

source

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

x ≠ cardano_formula_a f c d c_ne_zero → x ≠ cardano_formula_b f c d c_ne_zero → x ≠ cardano_formula_c f c d c_ne_zero → depressed_cubic_subst f c d x ≠ myfld.zero

source

theorem cubic_formula_uniqueness (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (a1 b c d x : f) (a_ne_zero : a1 ≠ myfld.zero) (int_quantity_ne_zero : (three f) .* (a1 .* c) .+ .- (square f b) ≠ myfld.zero) :

x ≠ cubic_formula_a f a1 b c d a_ne_zero int_quantity_ne_zero → x ≠ cubic_formula_b f a1 b c d a_ne_zero int_quantity_ne_zero → x ≠ cubic_formula_c f a1 b c d a_ne_zero int_quantity_ne_zero → cubic_subst f a1 b c d x ≠ myfld.zero

source

theorem cubic_formula_alt_uniqueness (f : Type) [myfld f] [fld_with_sqrt f] [fld_with_cube_root f] [fld_not_char_two f] [fld_not_char_three f] (a1 b c d x : f) (a_ne_zero : a1 ≠ myfld.zero) (int_quantity_eq_zero : (three f) .* (a1 .* c) .+ .- (square f b) = myfld.zero) :

x ≠ cubic_formula_a_alt f a1 b c d a_ne_zero int_quantity_eq_zero → x ≠ cubic_formula_b_alt f a1 b c d a_ne_zero int_quantity_eq_zero → x ≠ cubic_formula_c_alt f a1 b c d a_ne_zero int_quantity_eq_zero → cubic_subst f a1 b c d x ≠ myfld.zero