mathlib documentation

non-mathlib.roots

source
@[class]
structure fld_with_sqrt (f : Type) [myfld f] :
Type
source
theorem sqrt_eq (f : Type) [myfld f] [fld_with_sqrt f] (a b : f) :
a = b → sqroot a = sqroot b
source
@[simp]
theorem sqrt_simp (f : Type) [myfld f] [fld_with_sqrt f] (a : f) :
sqroot a .* sqroot a = a
source
@[simp]
theorem sqrt_squared (f : Type) [myfld f] [fld_with_sqrt f] (a : f) :
square f sqroot a = a
source
theorem only_two_square_roots (f : Type) [myfld f] [fld_with_sqrt f] (x y : f) :
x ≠ sqroot y → x ≠ .- sqroot y → square f x ≠ y
source
theorem negative_sqrt (f : Type) [myfld f] [fld_with_sqrt f] (a : f) :
.- sqroot a .* .- sqroot a = a
source
theorem sqrt_ne_zero (f : Type) [myfld f] [fld_with_sqrt f] (a : f) :
a ≠ myfld.zero → sqroot a ≠ myfld.zero
source
@[class]
structure fld_with_cube_root (f : Type) [myfld f] :
Type
source
theorem cubrt_eq (f : Type) [myfld f] [fld_with_cube_root f] (a b : f) :
a = b → fld_with_cube_root.cubrt a = fld_with_cube_root.cubrt b
source
theorem cubrt_cubed (f : Type) [myfld f] [fld_with_cube_root f] (a : f) :
cubed f (fld_with_cube_root.cubrt a) = a
source
def cubrt_nonzero (f : Type) [myfld f] [fld_with_cube_root f] (a : f) :
a ≠ myfld.zero → fld_with_cube_root.cubrt a ≠ myfld.zero
source
def cube_root_of_unity (f : Type) [myfld f] [fld_not_char_two f] (rt_minus_three : f) (rt_proof : rt_minus_three .* rt_minus_three = .- (three f)) :
f
Equations
source
theorem cubrt_unity_correct (f : Type) [myfld f] [fld_not_char_two f] (rt_minus_three : f) (rt_proof : rt_minus_three .* rt_minus_three = .- (three f)) :
cubed f (cube_root_of_unity f rt_minus_three rt_proof) = myfld.one
source
def cubrt_unity_a (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] :
f
Equations
source
def cubrt_unity_b (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] :
f
Equations
source
theorem cubrts_unity_sum_zero (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] :
myfld.one .+ ((cubrt_unity_a f) .+ (cubrt_unity_b f)) = myfld.zero
source
theorem no_other_cubrts_unity_sub_proof_a (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] [fld_with_cube_root f] (a x : f) :
.- (((fld_with_cube_root.cubrt a) .+ ((fld_with_cube_root.cubrt a) .* (cubrt_unity_a f) .+ (fld_with_cube_root.cubrt a) .* (cubrt_unity_b f))) .* (x .* x)) = myfld.zero
source
theorem no_other_cubrts_unity_sub_proof_b (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] [fld_with_cube_root f] (a x : f) :
x .* ((fld_with_cube_root.cubrt a) .* ((fld_with_cube_root.cubrt a) .* (cubrt_unity_a f)) .+ (fld_with_cube_root.cubrt a) .* ((fld_with_cube_root.cubrt a) .* (cubrt_unity_b f)) .+ (fld_with_cube_root.cubrt a) .* (cubrt_unity_a f) .* ((fld_with_cube_root.cubrt a) .* (cubrt_unity_b f))) = myfld.zero
source
theorem no_other_cubrts (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] [fld_with_cube_root f] (a x : f) :
x ≠ fld_with_cube_root.cubrt a → x ≠ (fld_with_cube_root.cubrt a) .* (cubrt_unity_a f) → x ≠ (fld_with_cube_root.cubrt a) .* (cubrt_unity_b f) → cubed f x ≠ a
source
theorem cubrt_unity_nonzero (f : Type) [myfld f] [fld_not_char_two f] (rt_minus_three : f) (rt_proof : rt_minus_three .* rt_minus_three = .- (three f)) :
cube_root_of_unity f rt_minus_three rt_proof ≠ myfld.zero
source
def alt_cubrt_a (f : Type) [myfld f] [fld_with_cube_root f] [fld_with_sqrt f] [fld_not_char_two f] (a : f) :
f
Equations
source
theorem alt_cubrt_a_nonzero (f : Type) [myfld f] [fld_with_cube_root f] [fld_with_sqrt f] [fld_not_char_two f] (a : f) (a_ne_zero : a ≠ myfld.zero) :
alt_cubrt_a f a ≠ myfld.zero
source
def alt_cubrt_b (f : Type) [myfld f] [fld_with_cube_root f] [fld_with_sqrt f] [fld_not_char_two f] (a : f) :
f
Equations
source
theorem alt_cubrt_b_nonzero (f : Type) [myfld f] [fld_with_cube_root f] [fld_with_sqrt f] [fld_not_char_two f] (a : f) (a_ne_zero : a ≠ myfld.zero) :
alt_cubrt_b f a ≠ myfld.zero
source
theorem three_cubrts (f : Type) [myfld f] [fld_not_char_two f] [fld_with_cube_root f] (rt_minus_three a : f) (rt_proof : rt_minus_three .* rt_minus_three = .- (three f)) :
cubed f (fld_with_cube_root.cubrt a) .* (cube_root_of_unity f rt_minus_three rt_proof) = a
source
theorem no_other_cubrts_simple (f : Type) [myfld f] [fld_with_sqrt f] [fld_not_char_two f] [fld_with_cube_root f] (a1 x : f) :
x ≠ fld_with_cube_root.cubrt a1 → x ≠ alt_cubrt_a f a1 → x ≠ alt_cubrt_b f a1 → cubed f x ≠ a1
source
theorem alt_cubrt_a_correct (f : Type) [myfld f] [fld_with_cube_root f] [fld_with_sqrt f] [fld_not_char_two f] (a : f) :
cubed f (alt_cubrt_a f a) = a
source
theorem alt_cubrt_b_correct (f : Type) [myfld f] [fld_with_cube_root f] [fld_with_sqrt f] [fld_not_char_two f] (a : f) :
cubed f (alt_cubrt_b f a) = a