Defs

📁 Source: Mathlib/Algebra/BrauerGroup/Defs.lean

Statistics

Metric	Count
Definitions CSA_Setoid, BrauerGroup, CSA, toAlgCat, IsBrauerEquivalent, instCoeSortCSAType	6
Theorems fin_dim, isCentral, isSimple, is_eqv, refl, trans	6
Total	12

Brauer

Definitions

Name	Category	Theorems
CSA_Setoid 📖	CompOp	—

CSA

Definitions

Name	Category	Theorems
toAlgCat 📖	CompOp	3 math math: isSimple, fin_dim, isCentral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fin_dim 📖	mathematical	—	FiniteDimensional AlgCat.carrier EuclideanDomain.toCommRing Field.toEuclideanDomain toAlgCat Field.toDivisionRing Ring.toAddCommGroup AlgCat.isRing Algebra.toModule Semifield.toCommSemiring Field.toSemifield Ring.toSemiring AlgCat.isAlgebra	—	—
isCentral 📖	mathematical	—	Algebra.IsCentral Semifield.toCommSemiring Field.toSemifield AlgCat.carrier EuclideanDomain.toCommRing Field.toEuclideanDomain toAlgCat Ring.toSemiring AlgCat.isRing AlgCat.isAlgebra	—	—
isSimple 📖	mathematical	—	IsSimpleRing AlgCat.carrier EuclideanDomain.toCommRing Field.toEuclideanDomain toAlgCat NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AlgCat.isRing	—	—

IsBrauerEquivalent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
is_eqv 📖	mathematical	—	CSA IsBrauerEquivalent	—	refl symm trans
refl 📖	mathematical	—	IsBrauerEquivalent	—	one_ne_zero
trans 📖	—	IsBrauerEquivalent	—	—	IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd

(root)

Definitions

Name	Category	Theorems
BrauerGroup 📖	CompOp	—
CSA 📖	CompData	1 math math: IsBrauerEquivalent.is_eqv
IsBrauerEquivalent 📖	MathDef	2 math math: IsBrauerEquivalent.refl, IsBrauerEquivalent.is_eqv
instCoeSortCSAType 📖	CompOp	—

---

← Back to Index