CategoryTheory

📁 Source: Mathlib/LinearAlgebra/CliffordAlgebra/CategoryTheory.lean

Statistics

Metric	Count
Definitions cliffordAlgebra	1
Theorems cliffordAlgebra_map, cliffordAlgebra_obj_carrier	2
Total	3

QuadraticModuleCat

Definitions

Name	Category	Theorems
cliffordAlgebra 📖	CompOp	2 math math: cliffordAlgebra_map, cliffordAlgebra_obj_carrier

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cliffordAlgebra_map 📖	mathematical	—	CategoryTheory.Functor.map QuadraticModuleCat category AlgCat AlgCat.instCategory cliffordAlgebra AlgCat.ofHom CliffordAlgebra ModuleCat.carrier CommRing.toRing toModuleCat ModuleCat.isAddCommGroup ModuleCat.isModule form instRingCliffordAlgebra instAlgebraCliffordAlgebra CliffordAlgebra.map Hom.toIsometry	—	—
cliffordAlgebra_obj_carrier 📖	mathematical	—	AlgCat.carrier CategoryTheory.Functor.obj QuadraticModuleCat category AlgCat AlgCat.instCategory cliffordAlgebra CliffordAlgebra ModuleCat.carrier CommRing.toRing toModuleCat ModuleCat.isAddCommGroup ModuleCat.isModule form	—	—

---

← Back to Index