Documentation

banach_tarski.Definitions

def matrix_a :
Matrix (Fin 3) (Fin 3)
Equations
def matrix_a' :
Matrix (Fin 3) (Fin 3)
Equations
def matrix_b :
Matrix (Fin 3) (Fin 3)
Equations
def matrix_b' :
Matrix (Fin 3) (Fin 3)
Equations
def matrix_one :
Matrix (Fin 3) (Fin 3)
Equations
def erzeuger :
Set (GL (Fin 3) )
Equations
@[inline, reducible]
abbrev r_3 :
Equations
@[inline, reducible]
abbrev r_2 :
Equations
Equations
def rotate (p : GL (Fin 3) ) (vec : r_3) :
Equations
def rotate_set (x : Set r_3) (p : GL (Fin 3) ) :
Equations
def rotate_n_times (n : ) (p : GL (Fin 3) ) (vec : r_3) :
Equations
def translate (p : r_3) (vec : r_3) :
Equations
def L :
Equations
def origin :
Equations
def L' :
Equations
def fixpunkt (y : r_3) (p : GL (Fin 3) ) :
Equations
def D :
Set L'
Equations
def rotationsAchse (p : GL (Fin 3) ) :
Equations
@[inline, reducible]
abbrev G_list :
Equations
Equations