mathlib documentation

non-mathlib.quadratic

def quadratic_subst (f : Type) [myfld f] :

f → f → f → f → f

Equations

quadratic_subst f x a b c = a .* (x .* x) .+ (b .* x .+ c)

theorem complete_the_square (f : Type) [myfld f] (x b : f) :

x .* x .+ (two f) .* b .* x = (square f x .+ b) .+ .- (square f b)

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

square f x .+ a = (square f x) .+ ((two f) .* (a .* x) .+ (square f a))

def quadratic_formula (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] (a b c : f) (a_ne_zero : a ≠ myfld.zero) :

f

Equations

quadratic_formula f a b c a_ne_zero = ( .- b .+ sqroot (b .* b .+ .- ((four f) .* (a .* c)))) .* (myfld.reciprocal (two f) .* a _)

theorem quadratic_formula_sub_proof_a (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] (a b c sqrt : f) (a_ne_zero : a ≠ myfld.zero) :

a .* ( .- b .* (myfld.reciprocal (two f) .* a _) .* ( .- b .* (myfld.reciprocal (two f) .* a _))) .+ a .* ( .- b .* (myfld.reciprocal (two f) .* a _) .* (sqrt .* (myfld.reciprocal (two f) .* a _))) .+ (a .* (sqrt .* (myfld.reciprocal (two f) .* a _) .* ( .- b .* (myfld.reciprocal (two f) .* a _))) .+ a .* (sqrt .* (myfld.reciprocal (two f) .* a _) .* (sqrt .* (myfld.reciprocal (two f) .* a _)))) .+ (b .* ( .- b .* (myfld.reciprocal (two f) .* a _)) .+ b .* (sqrt .* (myfld.reciprocal (two f) .* a _)) .+ c) = c .+ (myfld.reciprocal (two f) .* a _) .* (b .* (b .* (myfld.reciprocal (two f) _)) .+ (sqrt .* ((myfld.reciprocal (two f) _) .* sqrt) .+ .- b .* b))

theorem quadratic_formula_sub_proof_b (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] (a b c : f) (a_ne_zero : a ≠ myfld.zero) :

c .+ (myfld.reciprocal (two f) .* a _) .* (b .* (b .* (myfld.reciprocal (two f) _)) .+ (b .* b .* (myfld.reciprocal (two f) _) .+ .- ((four f) .* (a .* c)) .* (myfld.reciprocal (two f) _) .+ .- b .* b)) = myfld.zero

theorem quadratic_formula_works (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] (a b c : f) (a_ne_zero : a ≠ myfld.zero) :

quadratic_subst f (quadratic_formula f a b c a_ne_zero) a b c = myfld.zero

def quadratic_formula_alt (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] (a b c : f) (a_ne_zero : a ≠ myfld.zero) :

f

Equations

quadratic_formula_alt f a b c a_ne_zero = ( .- b .+ .- sqroot (b .* b .+ .- ((four f) .* (a .* c)))) .* (myfld.reciprocal (two f) .* a _)

theorem quadratic_formula_alt_works (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] (a b c : f) (a_ne_zero : a ≠ myfld.zero) :

quadratic_subst f (quadratic_formula_alt f a b c a_ne_zero) a b c = myfld.zero

theorem quadratic_solution_unique (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] (a b c x : f) (a_ne_zero : a ≠ myfld.zero) :

x ≠ quadratic_formula f a b c a_ne_zero ∧ x ≠ quadratic_formula_alt f a b c a_ne_zero → quadratic_subst f x a b c ≠ myfld.zero

theorem quadratic_factorize (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] (b c x : f) :

(x .+ .- (quadratic_formula f myfld.one b c myfld.zero_distinct_one)) .* (x .+ .- (quadratic_formula_alt f myfld.one b c myfld.zero_distinct_one)) = quadratic_subst f x myfld.one b c