mathlib documentation

non-mathlib.field_definition

source
@[class]
structure myfld (f : Type) :
Type
source
def square (f : Type) [myfld f] :
f → f
Equations
source
@[simp]
theorem add_comm (f : Type) [myfld f] (x y : f) :
x .+ y = y .+ x
source
@[simp]
theorem one_mul_simp (f : Type) [myfld f] (x : f) :
myfld.one .* x = x
source
@[simp]
theorem add_assoc (f : Type) [myfld f] (x y z : f) :
x .+ y .+ z = x .+ (y .+ z)
source
@[simp]
theorem mul_comm (f : Type) [myfld f] (x y : f) :
x .* y = y .* x
source
@[simp]
theorem mul_assoc (f : Type) [myfld f] (x y z : f) :
x .* y .* z = x .* (y .* z)
source
theorem zero_add (f : Type) [myfld f] (x : f) :
x = myfld.zero .+ x
source
@[simp]
theorem zero_simp (f : Type) [myfld f] (x : f) :
x .+ myfld.zero = x
source
@[simp]
theorem simp_zero (f : Type) [myfld f] (x : f) :
myfld.zero .+ x = x
source
@[simp]
theorem distrib_simp (f : Type) [myfld f] (x y z : f) :
(x .+ y) .* z = x .* z .+ y .* z
source
@[simp]
theorem distrib_simp_alt (f : Type) [myfld f] (x y z : f) :
x .* (y .+ z) = x .* y .+ x .* z
source
@[simp]
theorem one_mul (f : Type) [myfld f] (x : f) :
myfld.one .* x = x
source
@[simp]
theorem simp_mul_one (f : Type) [myfld f] (x : f) :
x .* myfld.one = x
source
@[simp]
theorem add_negate_simp (f : Type) [myfld f] (x : f) :
x .+ .- x = myfld.zero
source
@[simp]
theorem add_negate_simp_alt (f : Type) [myfld f] (x : f) :
.- x .+ x = myfld.zero
source
@[simp]
theorem mul_reciprocal (f : Type) [myfld f] (x : f) (proof : x ≠ myfld.zero) :
x .* (myfld.reciprocal x proof) = myfld.one
source
theorem equal_ne_zero (f : Type) [myfld f] (x y : f) :
x = y → x ≠ myfld.zero → y ≠ myfld.zero