mathlib3 documentation

lean-ga / geometric_algebra.translations.laurents

Derived from "A Formalization of Grassmann-Cayley Algebra in Coq and Its Application to Theorem Proving in Projective Geometry" #

by Laurent Fuchs and Laurent Théry

source
def laurent.Kₙ (α : Type) [field α] :
ℕ → Type
Equations
Instances for laurent.Kₙ
source
@[protected, instance]
def laurent.Kₙ.add_comm_group (α : Type) [field α] (n : ℕ) :
add_comm_group (laurent.Kₙ α n)
Equations
source
@[protected, instance]
def laurent.Kₙ.module (α : Type) [field α] (n : ℕ) :
module α (laurent.Kₙ α n)
Equations
source
def laurent.Gₙ (α : Type) [field α] :
ℕ → Type
Equations
Instances for laurent.Gₙ
source
@[protected, instance]
def laurent.Gₙ.add_comm_group (α : Type) [field α] (n : ℕ) :
add_comm_group (laurent.Gₙ α n)
Equations
source
def laurent.coe_α {α : Type} [field α] {n : ℕ} :
α → laurent.Gₙ α n
Equations
source
@[protected, instance]
def laurent.has_coe_α {α : Type} [field α] (n : ℕ) :
has_coe α (laurent.Gₙ α n)
Equations
source
def laurent.coe_Kₙ {α : Type} [field α] {n : ℕ} :
laurent.Kₙ α n → laurent.Gₙ α n
Equations
source
@[protected, instance]
def laurent.has_coe_Kₙ {α : Type} [field α] (n : ℕ) :
has_coe (laurent.Kₙ α n) (laurent.Gₙ α n)
Equations
source
def laurent.conj {α : Type} [field α] {n : ℕ} :
laurent.Gₙ α n → laurent.Gₙ α n
Equations
source
def laurent.conj_d {α : Type} [field α] {n : ℕ} :
laurent.Gₙ α n → laurent.Gₙ α n
Equations
source
def laurent.vee {α : Type} [field α] {n : ℕ} :
laurent.Gₙ α n → laurent.Gₙ α n → laurent.Gₙ α n
Equations
source
def laurent.wedge {α : Type} [field α] {n : ℕ} :
laurent.Gₙ α n → laurent.Gₙ α n → laurent.Gₙ α n
Equations