Documentation

LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.Span

Imports

Init
Mathlib.Tactic.SetLike
Mathlib.Data.Finset.Attr
Mathlib.Tactic.Bound.Init
Mathlib.Tactic.Finiteness.Attr
LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.Span.Basic

Imported by

Brauer Group New Mathlib Span #

Import index for the Brauer group formalization.