non-mathlib.field_results

source

theorem mul_cancel (f : Type) [myfld f] (a b x : f) (x_ne_zero : x ≠ myfld.zero) :

a .* x = b .* x → a = b

source

theorem add_cancel (f : Type) [myfld f] (a b x : f) :

a = b → x .+ a = x .+ b

source

theorem add_cancel_inv (f : Type) [myfld f] (a b x : f) :

a .+ x = b .+ x → a = b

source

theorem only_one_reciprocal (f : Type) [myfld f] (x : f) (a b : x ≠ myfld.zero) :

myfld.reciprocal x a = myfld.reciprocal x b

source

@[simp]

theorem mul_zero (f : Type) [myfld f] (x : f) :

myfld.zero .* x = myfld.zero

source

@[simp]

theorem zero_mul (f : Type) [myfld f] (x : f) :

x .* myfld.zero = myfld.zero

source

theorem only_one_reciprocal_alt (f : Type) [myfld f] (a b : f) (a_ne_zero : a ≠ myfld.zero) :

a .* b = myfld.one → b = myfld.reciprocal a a_ne_zero

source

@[simp]

theorem negate_zero_zero (f : Type) [myfld f] :

.- myfld.zero = myfld.zero

source

theorem negate_ne_zero (f : Type) [myfld f] (a : f) :

a ≠ myfld.zero → .- a ≠ myfld.zero

source

@[simp]

theorem recip_one_one (f : Type) [myfld f] (one_ne_zero : myfld.one ≠ myfld.zero) :

myfld.reciprocal myfld.one one_ne_zero = myfld.one

source

@[simp]

theorem double_negative (f : Type) [myfld f] (x : f) :

.- .- x = x

source

theorem reciprocal_ne_zero (f : Type) [myfld f] (x : f) (x_ne_zero : x ≠ myfld.zero) :

myfld.reciprocal x x_ne_zero ≠ myfld.zero

source

@[simp]

theorem double_reciprocal (f : Type) [myfld f] (x : f) (x_ne_zero : x ≠ myfld.zero) :

myfld.reciprocal (myfld.reciprocal x x_ne_zero) _ = x

source

theorem double_reciprocal_inv (f : Type) [myfld f] (x : f) (x_ne_zero : x ≠ myfld.zero) :

x = myfld.reciprocal (myfld.reciprocal x x_ne_zero) _

source

@[simp]

theorem mul_negate (f : Type) [myfld f] (x y : f) :

.- x .* y = .- (x .* y)

source

@[simp]

theorem mul_negate_alt_simp (f : Type) [myfld f] (x y : f) :

x .* .- y = .- (x .* y)

source

theorem mul_negate_alt (f : Type) [myfld f] (x y : f) :

.- (x .* y) = x .* .- y

source

@[simp]

theorem add_negate (f : Type) [myfld f] (x y : f) :

.- (x .+ y) = .- x .+ .- y

source

theorem mul_nonzero (f : Type) [myfld f] (x y : f) (x_ne_zero : x ≠ myfld.zero) (y_ne_zero : y ≠ myfld.zero) :

x .* y ≠ myfld.zero

source

@[simp]

theorem mul_two_reciprocals (f : Type) [myfld f] (x y : f) (x_ne_zero : x ≠ myfld.zero) (y_ne_zero : y ≠ myfld.zero) :

(myfld.reciprocal x x_ne_zero) .* (myfld.reciprocal y y_ne_zero) = myfld.reciprocal x .* y _

source

theorem factor_1_ne_zero (f : Type) [myfld f] (x y : f) :

x .* y ≠ myfld.zero → x ≠ myfld.zero

source

theorem factor_2_ne_zero (f : Type) [myfld f] (x y : f) :

x .* y ≠ myfld.zero → y ≠ myfld.zero

source

theorem split_reciprocal (f : Type) [myfld f] (x y : f) (xy_ne_zero : x .* y ≠ myfld.zero) :

myfld.reciprocal x .* y xy_ne_zero = (myfld.reciprocal x _) .* (myfld.reciprocal y _)

source

theorem cancel_from_reciprocal (f : Type) [myfld f] (x y : f) (xy_ne_zero : x .* y ≠ myfld.zero) :

(myfld.reciprocal x .* y xy_ne_zero) .* x = myfld.reciprocal y _

source

theorem cancel_from_reciprocal_alt (f : Type) [myfld f] (x y : f) (xy_ne_zero : x .* y ≠ myfld.zero) :

x .* (myfld.reciprocal x .* y xy_ne_zero) = myfld.reciprocal y _

source

theorem add_two_reciprocals (f : Type) [myfld f] (x y : f) (x_ne_zero : x ≠ myfld.zero) (y_ne_zero : y ≠ myfld.zero) :

(myfld.reciprocal x x_ne_zero) .+ (myfld.reciprocal y y_ne_zero) = (x .+ y) .* (myfld.reciprocal x .* y _)

source

theorem only_one_negation (f : Type) [myfld f] (a b : f) :

a .+ b = myfld.zero → b = .- a

source

theorem reciprocal_rewrite (f : Type) [myfld f] (x y : f) (equal_proof : x = y) (x_ne_zero : x ≠ myfld.zero) :

myfld.reciprocal x x_ne_zero = myfld.reciprocal y _

source

theorem assoc_tree (f : Type) [myfld f] (a b c d : f) :

a .+ b .+ (c .+ d) = a .+ (b .+ c .+ d)

source

theorem assoc_tree_mul (f : Type) [myfld f] (a b c d : f) :

a .* b .* (c .* d) = a .* (b .* c .* d)

source

theorem multiply_two_squares (f : Type) [myfld f] (a b : f) :

(square f a) .* (square f b) = square f a .* b

source

theorem mul_zero_by_reciprocal (f : Type) [myfld f] (a b : f) (a_ne_zero : a ≠ myfld.zero) :

b = myfld.zero ↔ b .* (myfld.reciprocal a a_ne_zero) = myfld.zero

source

theorem negate_zero (f : Type) [myfld f] (a : f) :

a = myfld.zero ↔ .- a = myfld.zero

source

theorem negate_zero_a (f : Type) [myfld f] (a : f) :

a = myfld.zero → .- a = myfld.zero

source

theorem carry_term_across (f : Type) [myfld f] (a b x : f) :

a .+ x = b ↔ a = b .+ .- x

source

theorem carry_term_across_alt (f : Type) [myfld f] (a b : f) :

a = b ↔ myfld.zero = b .+ .- a

source

theorem mul_both_sides (f : Type) [myfld f] (a b x : f) (x_ne_zero : x ≠ myfld.zero) :

a = b ↔ a .* x = b .* x

source

theorem mul_both_sides_ne (f : Type) [myfld f] (a b x : f) :

a ≠ b → x ≠ myfld.zero → a .* x ≠ b .* x

source

theorem carry_term_across_ne (f : Type) [myfld f] (a b x : f) :

a .+ x ≠ b ↔ a ≠ b .+ .- x

source

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

f → f

Equations

cubed f a = a .* (a .* a)

source

def cube_of_product (f : Type) [myfld f] (a b : f) :

cubed f a .* b = (cubed f a) .* (cubed f b)

source

def cube_nonzero (f : Type) [myfld f] (a : f) :

a ≠ myfld.zero → cubed f a ≠ myfld.zero

source

def cube_of_negative (f : Type) [myfld f] (a : f) :

cubed f .- a = .- (cubed f a)

source

def cube_of_reciprocal (f : Type) [myfld f] (a : f) (a_ne_zero : a ≠ myfld.zero) :

cubed f (myfld.reciprocal a a_ne_zero) = myfld.reciprocal (cubed f a) _

source

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

f

Equations

factorized_cubic_expression f x a b c = (x .+ .- a) .* (x .+ .- b) .* (x .+ .- c)

source

theorem ne_diff_not_zero (f : Type) [myfld f] (x y : f) :

x ≠ y → x .+ .- y ≠ myfld.zero

source

theorem multiply_out_cubic (f : Type) [myfld f] (x a b c : f) :

factorized_cubic_expression f x a b c = (cubed f x) .+ ( .- ((a .+ (b .+ c)) .* (x .* x)) .+ (x .* (a .* b .+ a .* c .+ b .* c) .+ .- (a .* (b .* c))))

source

theorem difference_of_squares (f : Type) [myfld f] (a b : f) :

(a .+ b) .* (a .+ .- b) = (square f a) .+ .- (square f b)

source

theorem mul_complex (f : Type) [myfld f] (a b c d : f) :

a .* (b .* c) .* (a .* (d .* c)) = a .* c .* (a .* c) .* (b .* d)

source

theorem subtract_ne (f : Type) [myfld f] (a b : f) :

a ≠ b → a .+ .- b ≠ myfld.zero

source

theorem move_negation_ne (f : Type) [myfld f] (a b : f) :

a ≠ .- b ↔ .- a ≠ b

source

theorem move_across (f : Type) [myfld f] (a b : f) :

a .+ b = myfld.zero ↔ .- a = b

source

@[simp]

theorem square_negate (f : Type) [myfld f] (a : f) :

square f .- a = square f a

source

@[simp]

theorem cube_negate (f : Type) [myfld f] (a : f) :

cubed f .- a = .- (cubed f a)

source

theorem mul_two_squares (f : Type) [myfld f] (a b : f) :

(square f a) .* (square f b) = square f a .* b

source

theorem square_ne_zero (f : Type) [myfld f] (a : f) (a_ne_zero : a ≠ myfld.zero) :

square f a ≠ myfld.zero

source

theorem reciprocal_squared (f : Type) [myfld f] (a : f) (a_ne_zero : a ≠ myfld.zero) :

square f (myfld.reciprocal a a_ne_zero) = myfld.reciprocal (square f a) _