LeanPool.BrauerGroupNew.Subfield.FiniteDimensional #
Imported Lean Pool material for LeanPool.BrauerGroupNew.Subfield.FiniteDimensional.
instance
SubField.instFiniteDimensionalSubtypeMem
{K : Type u_1}
{A : Type u_2}
[Field K]
[Ring A]
[Algebra K A]
{L : SubField K A}
[FiniteDimensional K A]
:
FiniteDimensional K ↥L