Theorem B in the independent vocabulary #
The independent family is a skeleton of the proof library; its standardness
there (theoremB) transfers to the independent mesh category, because the
independent translate is the translation of Γ_A (translateCompatible) and
the coefficients of the mesh relations normalize to one (Lemma 4.4).
theorem
MultiplicativeBasisDeformations.Statement.theoremB
(k A : Type u)
[Field k]
[Ring A]
[Algebra k A]
[IsAlgClosed k]
[FiniteDimensional k A]
:
TheoremB k A
Theorem B in the independent vocabulary.