mathlib documentation

non-mathlib.numbers

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

f

Equations

two f = myfld.one .+ myfld.one

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

f

Equations

four f = (two f) .+ (two f)

@[class]

structure fld_not_char_two (f : Type) [myfld f] :

Type

not_char_two : myfld.one .+ myfld.one ≠ myfld.zero

theorem two_ne_zero (f : Type) [myfld f] [fld_not_char_two f] :

two f ≠ myfld.zero

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

(two f) .+ (two f) = (two f) .* (two f)

theorem four_ne_zero (f : Type) [myfld f] [fld_not_char_two f] :

four f ≠ myfld.zero

theorem add_two_halves (f : Type) [myfld f] [fld_not_char_two f] :

(myfld.reciprocal (two f) _) .+ (myfld.reciprocal (two f) _) = myfld.one

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

f

Equations

three f = myfld.one .+ (myfld.one .+ myfld.one)

@[class]

structure fld_not_char_three (f : Type) [myfld f] :

Type

not_char_three : three f ≠ myfld.zero

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

f

Equations

six f = (two f) .* (three f)

theorem six_ne_zero (f : Type) [myfld f] [fld_not_char_two f] [fld_not_char_three f] :

six f ≠ myfld.zero

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

f

Equations

nine f = (three f) .* (three f)

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

nine f ≠ myfld.zero

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

f

Equations

twenty_seven f = (three f) .* (nine f)

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

twenty_seven f ≠ myfld.zero

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

cubed f (three f) = twenty_seven f

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

(three f) .* (three f) .+ .- myfld.one = cubed f (two f)

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

myfld.one .+ (three f) = (two f) .* (two f)

theorem two_x_div_two (f : Type) [myfld f] [fld_not_char_two f] (a : f) :

(myfld.reciprocal (two f) fld_not_char_two.not_char_two) .* (a .+ a) = a